sync: engine v12.19 baseline (96 commits) - #88
Merged
Conversation
…ding horizon 1. Scheduled bucket: sched_remaining_q + sched_release_q <= sched_anchor_q (prevents stranded reserve when release already consumed most of anchor) 2. Pending bucket: pending_horizon > 0 when pending_present != 0 (prevents malformed pending from promoting into invalid scheduled) 3. r==0 fast path now calls validate_reserve_shape() instead of only checking present bits (catches ghost fields on absent buckets) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- sched_present != 0 && sched_remaining_q == 0 -> CorruptState - pending_present != 0 && pending_remaining_q == 0 -> CorruptState Prevents ghost present flags from surviving touch and blocking close/reclaim/GC/free_slot paths downstream. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…checked + error code A. set_pnl_with_reserve: validates R_i <= max(PNL_i, 0) at entry before any mutation. The old_rel binding was dead — now serves as the guard. B. liquidate_at_oracle_internal: bankruptcy set_pnl(i, 0) now uses NoPositiveIncreaseAllowed per spec §8.5 step 8 for defense-in-depth. C. charge_fee_to_insurance: insurance_fund.balance addition now uses checked_add().ok_or(Overflow) instead of unchecked U128 + operator. D. reclaim_empty_account_not_atomic: fee_credits > 0 error code changed from Undercollateralized to CorruptState (positive fee_credits is always a state invariant violation per §2.1). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Critical defense-in-depth: all four equity functions now saturate BOTH positive and negative I256->i128 overflow to i128::MIN + 1. Previously, positive overflow saturated to i128::MAX, which would pass any > 0, > MM_req, or > IM_req gate trivially. Under configured bounds this is unreachable, but the old direction was a latent trap that could flip an exploit into working if any other corruption vector emerged. Now every overflow fails every gate. Affected functions: - account_equity_maint_raw - account_equity_init_raw - account_equity_withdraw_raw - account_equity_trade_open_raw Additional fixes: - resolve_market_not_atomic: finalize_side_reset errors propagated instead of swallowed with let _ = - garbage_collect_dust: insurance += dust_cap now uses checked_add Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…tion
Spec §4.7-4.9 changes:
1. ReserveMode now: UseAdmissionPair(h_min, h_max) | ImmediateReleaseResolvedOnly
| NoPositiveIncreaseAllowed. Old UseHLock(u64) and ImmediateRelease removed.
2. admit_fresh_reserve_h_lock: decides effective horizon at reserve creation.
- If matured + fresh <= residual: return admit_h_min (fast path)
- Else: return admit_h_max (slow path) and mark account sticky
- Sticky: once h_max required in an instruction, all later fresh reserve
on that same account in that instruction also uses h_max (§0 goal 45)
3. admit_outstanding_reserve_on_touch: accelerates existing reserve when
state admits h=1 (matured + reserve <= residual). Called at start of
touch_account_live_local.
4. ImmediateReleaseResolvedOnly: rejects on Live, allowed on Resolved only.
Live positive increases MUST go through UseAdmissionPair.
5. InstructionContext extended with:
- admit_h_min_shared, admit_h_max_shared
- h_max_sticky_accounts[MAX_TOUCHED_PER_INSTRUCTION]
- is_h_max_sticky(), mark_h_max_sticky()
6. All 7 public _not_atomic signatures updated: h_lock -> (admit_h_min, admit_h_max)
- settle_account, withdraw, convert_released_pnl, execute_trade,
close_account, keeper_crank, liquidate_at_oracle
7. validate_h_lock -> validate_admission_pair (spec §1.4 bounds):
0 <= admit_h_min <= admit_h_max <= cfg_h_max
if admit_h_min > 0, admit_h_min >= cfg_h_min
All 219 tests pass (167 unit + 49 fuzz + 3 AMM).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Added 10 proofs for v12.18 changes (all pass in ~0.4-0.7s each): Group AH (Admission with pair + sticky rule, spec §4.7): - AH-1: single admission returns exactly admit_h_min or admit_h_max - AH-2: sticky-h_max is absorbing (once sticky, always h_max) - AH-3: no under-admission (v12.18 core safety fix) - AH-4: h_min=0 admission preserves h=1 invariant - AH-5: cross-account sticky isolation - AH-6: admit_h_min > 0 is a floor (result >= h_min) Group AC (Acceleration on touch, spec §4.9): - AC-1: acceleration is all-or-nothing - AC-2: acceleration fires iff state admits - AC-4: acceleration preserves conservation & monotone matured Group IN (v12.18-specific invariants): - IN-1: ImmediateReleaseResolvedOnly rejected on Live Implementation changes: - Exposed admit_fresh_reserve_h_lock and admit_outstanding_reserve_on_touch as pub for test/kani features via cfg_attr(doc(hidden)) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Critical integration bug found by audit: admit_outstanding_reserve_on_touch was defined and proven but never actually called in touch_account_live_local. The acceleration mechanism for eligible reserves never fired, making v12.18's new §4.9 feature dead code in production. Changes: - touch_account_live_local: call admit_outstanding_reserve_on_touch BEFORE advance_profit_warmup (spec §6.5 step 4 before step 5) - Version header: v12.17.0 -> v12.18.0 - test_warmup_full_conversion_after_period: updated to account for acceleration firing earlier (during close-trade finalize when b's loss grows residual), making the profit convert to capital before slot3. Test now verifies final capital > initial capital instead of post-close > pre-slot3. All 219 tests pass; admission/acceleration Kani proofs still pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Spec §1.4: for live instructions that may create fresh reserve, admit_h_max > 0 and admit_h_max >= cfg_h_min. Previously, passing (0, 0) would let admission return 0 regardless of state, admitting all fresh PnL directly to matured and bypassing the h=1 invariant protection. A malicious or buggy wrapper could defeat the entire admission mechanism. Fix: validate_admission_pair rejects admit_h_max == 0. All 288 test call sites using (0, 0) updated to (0, 100) — they were relying on the old v12.17 ImmediateRelease semantics. Added Kani proof k9_admission_pair_rejects_zero_max (verified). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Bug 1 (CRITICAL, safety+liveness): accrue_market_to had no dt cap and init-time envelope wasn't validated. Dormant markets could accumulate unbounded F_side_num before triggering conservative overflow. - Added RiskParams.max_accrual_dt_slots and max_abs_funding_e9_per_slot - validate_params: init-time envelope check ADL_ONE * MAX_ORACLE_PRICE * rate_max * dt_max <= i128::MAX - accrue_market_to: per-call check dt <= max_accrual_dt_slots - accrue_market_to now uses per-market rate bound (not global constant) Bug 2 (CRITICAL, liveness): resolve_market_not_atomic had no degenerate recovery branch. Once envelope exceeded, market couldn't be resolved. Spec §9.8 clause 5: if live_oracle_price == P_last && funding_rate == 0, skip accrue_market_to entirely. This lets dormant markets resolve via terminal K deltas without triggering the dt cap. Added Kani proofs: - k1_accrue_rejects_dt_over_envelope: PASSES - k2_resolve_degenerate_bypasses_dt_cap: PASSES All 219 tests pass. Test params use dt_max=1000, rate_max=1e8. Test rates > 1e8 reduced to fit the envelope. test_accrue_market_to_multi_substep_large_dt (pre-v12.18 behavior) replaced with test_accrue_market_to_rejects_dt_over_envelope. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Bug 92 (MAJOR): materialize_with_fee violated validate-then-mutate contract.
c_tot += excess via checked_add could fail AFTER vault/insurance/account
mutations committed. Pre-validate by running checked_add first (dry-run)
before any state mutation.
Bug 73 (MEDIUM, defense-in-depth): close_resolved_terminal_not_atomic only
called prepare_account_for_resolved_touch in the pnl > 0 branch. For
pnl == 0 accounts with stale bucket metadata, free_slot would fail with
CorruptState. Now calls unconditionally before free_slot.
Kani proofs added (both verified):
- K-71: neg_pnl_account_count == actual count of used accounts with pnl < 0
after arbitrary set_pnl_with_reserve sequences.
- K-104: oi_eff_{long,short}_q >= sum of per-account effective_pos_q.
Also verifies bilateral OI invariant (long == short).
All 219 tests pass. 15 admission/invariant proofs all verified.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Bug 3: close_account_not_atomic must require FeeDebt_i == 0 (spec §9.5 step 11) - Removed fee debt forgiveness in voluntary close path - Added R_i == 0 and bucket-absent check per spec §9.5 step 10 Bug 4: liquidate_at_oracle_not_atomic must require materialized (spec §9.6 step 2) - Added AccountNotFound check on public entrypoint Bug 5: Degenerate resolve must skip band check (spec §9.8 step 8) - Restructured resolve_market_not_atomic to use used_degenerate flag - Band check now only runs on ordinary branch - Degenerate branch relies entirely on trusted wrapper inputs per §9.8 Bug 6: keeper_crank must not do dust GC (spec §9.7) - Removed garbage_collect_dust call from keeper_crank_not_atomic - Deployments should run reclaim_empty_account_not_atomic explicitly Bug 9: validate_reserve_shape must check horizons in [cfg_h_min, cfg_h_max] - Strengthened bucket validation per spec §1.4/§4.4 - sched_horizon and pending_horizon now validated against config bounds Test fix: test_advance_profit_warmup_sched_then_pending_promotion was using horizon=200 > cfg_h_max=100, now uses valid horizons within bounds. All 219 tests pass. All 15 admission proofs pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ecked_add Bug 163 (MEDIUM, spec §4.17): record_uninsured_protocol_loss was a no-op comment. When K-space overflow prevents ADL socialization, the uncovered deficit must be "represented through Residual" per spec. Now implemented as V reduction (capped at Residual so V >= C_tot + I preserved). Effect: after an uninsured bankruptcy, Residual shrinks. If this drops Residual below pnl_matured_pos_tot, haircut h < 1 kicks in on subsequent conversions, correctly socializing the loss to junior holders. Wired up at four sites: - enqueue_adl step 7 K-space checked_add overflow - enqueue_adl step 7 quotient OverI128Magnitude - enqueue_adl step 4 (OI_opp == 0, D_rem > 0) - enqueue_adl step 5 (no opp positions, D_rem > 0) Bug 109 (MINOR): Removed dead Ok(false) check after the new AccountNotFound guard in liquidate_at_oracle_not_atomic. Bug 155 (MINOR): Use explicit checked_add in deposit_not_atomic for insurance_fund.balance += required_fee (consistency with other sites). Bug 114 noted: validate_reserve_shape already applies [h_min, h_max] bounds to sched_horizon (added in prior commit 443de02). All 219 tests pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…audit
Strengthened 7 proofs that previously relied on hardcoded values:
- proof_effective_pos_q_flat_is_zero: now uses symbolic basis and
proper attach/detach path. Tests that after attaching a nonzero
position and detaching via attach(0), effective_pos_q returns 0.
Verification time: 11.6s (previously <1s tautology).
- proof_flat_zero_equity_not_maintenance_healthy: symbolic capital
and fee_debt where fee_debt >= cap forces Eq_net <= 0. Verifies
flat account with non-positive equity is NOT maintenance-healthy
across the full input space.
- proof_wide_signed_mul_div_floor_zero_inputs: symbolic k_diff,
basis, den values verify zero-factor short-circuit across space.
- proof_check_conservation_basic: symbolic V/C/I values verify
check_conservation returns exactly V >= C + I.
- proof_set_pnl_underflow_safety: symbolic pnl transitions via
the current admission-pair path. Verifies pnl_pos_tot tracks
max(pnl, 0) correctly across positive/negative transitions.
- proof_funding_skip_zero_oi_{long,short,both}: symbolic rate and dt
verify that funding K delta is zero when OI on either/both sides
is zero, regardless of rate magnitude.
All 7 proofs verified individually pass. The 33 proofs already
completed in the ongoing full-suite run also all pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Fixed 2 failing proofs and strengthened 3 more: Failed under v12.18 semantics (direct market_mode = Resolved bypass): - proof_force_close_resolved_with_position_conserves: now uses resolve_market_not_atomic for proper epoch increment. (FAILED → SUCCESSFUL 12.7s) - proof_force_close_resolved_pos_count_decrements: same fix. (FAILED → SUCCESSFUL 12.8s) Strengthened (direct mode-set OR set_pnl-on-Live rewritten): - proof_force_close_resolved_with_profit_conserves: now resolves first, then set_pnl via ImmediateReleaseResolvedOnly. Verification time went from passive (positive never set) to 71.4s (full state exploration). - proof_force_close_resolved_flat_returns_capital: uses resolve_market lifecycle. 3.5s. - proof_force_close_resolved_fee_sweep_conservation: uses resolve_market lifecycle. 3.5s. Also strengthened: - proof_set_position_basis_q_count_tracking: symbolic b1, b2 sign changes instead of hardcoded POS_SCALE transitions. 1.0s. All 5 strengthened proofs pass individually. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ive changes Individually verified each fix via cargo kani; full suite now green. Categories: - Missing-account / crank-gate (4): update expectations for Bug 4 Err(AccountNotFound) and the new max_accrual_dt_slots envelope. - set_pnl in Live mode (7): set_pnl uses ImmediateReleaseResolvedOnly which errs for positive increases in Live mode. Added set_pnl_test helper in tests/common that routes via UseAdmissionPair when needed, plus unwrap on the should_panic i128::MIN rejection. - Funding semantics (6): engine uses fund_px_last (not last_oracle_price) as the funding basis (v12.16.5, one exact delta, no K/F split). Tests now set fund_px_last explicitly and bound symbolic rates by the configured params.max_abs_funding_e9_per_slot (tighter than the global MAX_ABS_FUNDING_E9_PER_SLOT const). - Positive-overflow equity (2): commit 94df734 flipped saturation to fail-conservative (i128::MIN + 1). Proofs now assert the conservative behavior: overflow fails every gate. - close_account fee forgiveness (1): spec §9.5 step 11 requires FeeDebt == 0 before voluntary close. Fee forgiveness moved to the keeper-initiated reclaim_empty_account_not_atomic path. Proof updated. - Fee-shortfall routing (1): finalize_touched_accounts_post_live now auto-converts released PnL to capital and sweeps fee debt. Removed the set_pnl_with_reserve setup so there's no released PnL to convert; fee_credits stays negative as intended. - Convert-released-pnl (1): swapped keeper_crank touch order so b's loss settlement frees residual before a's fresh positive PnL is admitted — under v12.18 admission pair this routes to matured instead of reserve. - Partial liquidation (1): bumped kani::unwind to 256 for the U512 div/rem loop in wide_math. - Funding payer-driven (1): set fund_px_last so funding basis matches the test's expected values. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Engine surface now spec-conformant: deposit is the sole materialization path for missing accounts, with amount >= cfg_min_initial_deposit. No engine-native opening fee. Removed from engine: - RiskParams.new_account_fee field - materialize_with_fee() public method - add_user() / add_lp() test_visible wrappers - Fee routing branch in deposit_not_atomic Added to engine: - materialize_at() wrapped in test_visible! (was private) Tests: - New helpers add_user_test / add_lp_test in tests/common/mod.rs and inline in amm_tests.rs / unit_tests.rs / fuzzing.rs (test-only back-door via materialize_at, no capital change). - Dedicated spec-path tests: test_deposit_materialize_user, test_deposit_materialize_below_min_rejected, fix5_deposit_materialize_*. - Obsolete tests (test_add_user/test_add_user_with_excess/ test_add_user_insufficient_fee, test_materialize_then_dust_deposit_bypass, blocker6_invalid_kind_rejected) removed or reshaped. - All ~464 RiskParams instances stripped of new_account_fee field. - Kani proofs updated: proof_add_lp_count_rollback still valid. Verification: - cargo test --features test: 164 unit + 3 amm + all else pass - cargo test --features fuzz: 10 pass, 1 ignored - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replace compile-time MAX_ACTIVE_POSITIONS_PER_SIDE const with immutable RiskParams.max_active_positions_per_side per-market configuration. Engine: - New field: max_active_positions_per_side: u64 in RiskParams (spec §1.4) - Init-time invariant: 0 < max_active_positions_per_side <= max_accounts - set_position_basis_q enforces params.max_active_positions_per_side on long/short increments - Removed MAX_ACTIVE_POSITIONS_PER_SIDE const (no remaining references) Tests: - All 6 RiskParams factories (zero_fee_params, default_params, params_regime_a, params_regime_b in amm/unit/fuzzing) extended with max_active_positions_per_side: MAX_ACCOUNTS as u64 Verification: - cargo test --features test: all green (164 unit + 3 amm + rest) - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Revert record_uninsured_protocol_loss to a no-op. Draining V/Residual double-penalized junior holders (h haircut + V reduction), producing 0 payout where h = 0.5 is correct. Correct spec §4.17 semantics: after insurance is exhausted, the forgiven negative PnL leaves the matched positive PnL (matured_pos_tot) as an unchanged claim against Residual. When matured > residual, payouts scale by h = residual/matured — this IS how uninsured loss is represented. Shrinking V here would shrink residual below its post-forgiveness value and break that representation. Intuition (from external audit): Alice +100, Bob -100, V = 50, insurance = 0. Forgiving Bob leaves matured = 100, residual = 50 → h = 0.5, Alice gets 50. With V drained, residual = 0, Alice gets 0. Replaced implementation with doc-commented no-op; callers unchanged. Verification: cargo test --features test all green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three changes to ensure malformed reserve state fails conservatively instead of being "healed" by subsequent mutations: 1) validate_reserve_shape now enforces sched_horizon in [cfg_h_min, cfg_h_max] when sched_present != 0. Previously only pending_horizon was bounded-checked; malformed sched state could slip past. 2) touch_account_live_local calls validate_reserve_shape as the first post-mode/bounds check, BEFORE admit_outstanding_reserve_on_touch. Prevents corrupt reserve from being accelerated to matured. 3) append_or_route_new_reserve calls validate_reserve_shape at entry. Prevents merging fresh reserve on top of a bucket that violates shape invariants. Verification: - cargo test --features test: all green (164 + 49 + 3 + rest) - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
admit_fresh_reserve_h_lock now returns Result<u64> and uses checked arithmetic for senior/residual/matured_plus_fresh. Propagates ctx.mark_h_max_sticky failure as an error instead of silently dropping the sticky flag. Previous issues: - saturating_add/saturating_sub could mask overflow or a broken V >= C_tot + I invariant, producing an incorrect residual and a wrong admission decision at h_min when fail-conservative demands h_max. - mark_h_max_sticky return value was discarded. If the sticky list was full (MAX_TOUCHED_PER_INSTRUCTION), the account was not recorded as sticky; a later call in the same instruction could re-admit at h_min, violating the sticky-h_max invariant. New behavior: - senior = c_tot + insurance via checked_add; overflow → Err(Overflow). - residual = vault.checked_sub(senior); deficit → Err(CorruptState) (violates engine invariant; conservative fail). - matured_plus_fresh via checked_add; overflow → Err(Overflow). - mark_h_max_sticky returning false → Err(Overflow). Call sites: - set_pnl_with_reserve UseAdmissionPair branch now propagates via `?`. - 7 Kani proof call sites in proofs_admission.rs use .unwrap() (kani treats unwrap failures as unreachable on Ok paths). Verification: - cargo test --features test: all green - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Item 9 (keeper_crank max_revalidations): replace silent clamp-to-64 with an explicit Err(Overflow) when max_revalidations > MAX_TOUCHED_PER_INSTRUCTION. Silent truncation of requested work is a subtle liveness bug; fail explicitly instead. Existing callers already clamp or know the bound. Item 8 (public API surface): internal helpers no longer pub without _not_atomic. - admit_fresh_reserve_h_lock: was `pub fn` with cfg doc(hidden); now wrapped in test_visible! (private in production, pub in test/kani). Public callers should route through set_pnl_with_reserve / ReserveMode::UseAdmissionPair, which is the atomic entry point. - admit_outstanding_reserve_on_touch: was pub; now test_visible!. Called only by touch_account_live_local as part of the live-touch pipeline, which is itself a helper used by the _not_atomic entries. - run_end_of_instruction_lifecycle: was pub but had zero callers (internal or external). Removed entirely — dead code. The actual lifecycle is driven inline by each _not_atomic entry via schedule_end_of_instruction_resets + finalize_end_of_instruction_resets. Verification: - cargo test --features test: all green - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Every public _not_atomic entrypoint now asserts the global invariants at
its final success path:
assert_public_postconditions():
1. check_conservation(): V >= C_tot + I
2. oi_eff_long_q == oi_eff_short_q
Entrypoints (15 total, all covered):
deposit_not_atomic, withdraw_not_atomic, settle_account_not_atomic,
execute_trade_not_atomic, liquidate_at_oracle_not_atomic,
keeper_crank_not_atomic, convert_released_pnl_not_atomic,
close_account_not_atomic, resolve_market_not_atomic,
reconcile_resolved_not_atomic, close_resolved_terminal_not_atomic,
reclaim_empty_account_not_atomic, charge_account_fee_not_atomic,
settle_flat_negative_pnl_not_atomic.
force_close_resolved_not_atomic delegates to reconcile + terminal
close, both of which perform the check.
Previously some entrypoints asserted OI balance explicitly, a few didn't,
and conservation was implied by per-op checked arithmetic. The spec
requires both checks at the public surface regardless of internal
guarantees — this is defense-in-depth against any future per-op bug
that might silently break the invariants.
Verification:
- cargo test --features test: all green
- cargo kani --only-codegen: clean
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
close_resolved_terminal_not_atomic: swap consume_released_pnl to the canonical set_pnl_with_reserve(0, NoPositiveIncreaseAllowed) primitive. - consume_released_pnl is a Live-mode matured-drain helper (spec §4.4.1) that decrements pnl/pnl_pos_tot/pnl_matured_pos_tot by `released`. In Resolved mode after prepare_account_for_resolved_touch (reserve = 0) it happens to produce the correct end state, but it's semantically the wrong primitive. - set_pnl_with_reserve(i, 0, NoPositiveIncreaseAllowed, None) is the canonical PnL-mutation primitive (spec §4.5). Since new_pos (0) is not > old_pos, it doesn't hit the NoPositiveIncreaseAllowed rejection; instead it takes the Case B (no positive increase) path with the Resolved branch, decrementing pnl_matured_pos_tot by pos_loss. Same end state, consistent with the rest of the engine's API use. Also added a defense-in-depth assertion that reserved_pnl == 0 before using live-formula released_pos() in the resolved-close path. The invariant is guaranteed by prepare_account_for_resolved_touch, but checking it makes the Resolved-mode reliance on released_pos safe to verify. Not changed: - released_pos() keeps its live formula (max(pnl, 0) - reserved_pnl). In Resolved mode the engine invariant reserved_pnl == 0 makes it equivalent to max(pnl, 0); no correctness gap, and the single formula avoids a branch on market_mode in a view-only helper. Verification: - cargo test --features test: all green - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add four new Kani proofs that cover behavior introduced by items 5, 7, and 9. Each was designed to catch a specific regression class identified during proof-audit review. ah7_sticky_capacity_exhausted_fails (item 5): Fills the sticky list to capacity then invokes admit_fresh_reserve_h_lock in a state that requires h_max. Verifies the fallible signature returns Err instead of silently dropping the sticky flag (pre-fix bug: discarded bool). unwind(70) to unroll the 64-element fill loop. ah8_broken_conservation_fails (item 5): Breaks V >= C_tot + I and invokes the admission helper. Verifies that checked_sub(vault, senior) surfaces the broken invariant as Err(CorruptState) instead of silently returning 0 (pre-fix saturating_sub). k201_keeper_crank_rejects_oversized_budget (item 9): Symbolic over-MAX_TOUCHED_PER_INSTRUCTION request. Verifies the new explicit rejection path. Prevents regression of the silent clamp-to-64 behavior that masked caller intent. k202_postcondition_detects_broken_conservation (item 7): Forcibly breaks the V >= C_tot + I invariant, invokes a public _not_atomic entrypoint, and asserts it returns Err via assert_public_postconditions. Verifies the defense-in-depth postcondition actually fires. All four verified individually; also fit the existing full-suite run. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Addresses 5 real issues surfaced by independent proof-audit review. 1) validate_reserve_shape: enforce reserved_pnl <= max(pnl, 0) (spec §2.1). Previous check only validated bucket-metadata consistency; a corrupt account with reserve exceeding positive PnL could pass shape validation and be processed by downstream helpers. 2) admit_outstanding_reserve_on_touch: validate-then-mutate. Split into phase-1 (all checks with checked arithmetic, no mutation) and phase-2 (commit). Previously used saturating_add/sub which could mask overflow or broken conservation, and the new_matured > pnl_pos_tot check ran AFTER the reserve-clear mutations, violating the no-mutation-on-Err contract for a non-_not_atomic public helper. 3) apply_reserve_loss_newest_first: validate-then-mutate. Pre-compute take_pend and take_sched using existing bucket availability, verify reserve_loss <= total_avail AND reserve_loss <= reserved_pnl, only then mutate. Previously decremented buckets step-by-step and the "remaining != 0" check ran after partial consumption, leaving reserve state partially mutated on Err. 4) deposit_fee_credits: distinct error types. - Missing account: Unauthorized → AccountNotFound - Backward time: Unauthorized → Overflow Matches convention of the rest of the engine surface. 5) materialize_at: O(1) via doubly-linked free list. Added prev_free: [u16; MAX_ACCOUNTS] mirror of next_free. alloc_slot, free_slot, and materialize_at all maintain both pointers. materialize_at now unlinks at any position in constant time instead of linear-scanning up to MAX_ACCOUNTS (4096 in production). Fixes the worst-case compute cost of the missing-account deposit path. Regression proofs: - ac5_admit_outstanding_atomic_on_err: invariant break triggers Err with zero state change. - rs1_validate_rejects_reserved_exceeding_pos_pnl: corrupt reserve state rejected at append_or_route entry. Tests: - test_deposit_fee_credits_missing_account_returns_account_not_found - test_deposit_fee_credits_backwards_time_returns_overflow - Pre-existing test_append_reserve_* and test_apply_reserve_loss_newest_first updated to set backing pnl (spec §2.1 invariant now enforced). Verification: - cargo test --features test: 165 unit + 3 amm + 49 default + rest green - cargo kani --only-codegen: clean - 4 affected Kani proofs verified individually Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reviewer's pass 2 identified 2 real remaining gaps plus 1 ordering issue in the reserve-validation coverage: 1) admit_outstanding_reserve_on_touch did not call validate_reserve_shape at entry. A corrupt bucket (e.g., sched_remaining mismatching reserved_pnl, or reserved_pnl > max(pnl, 0)) could be accelerated through the helper — transforming corrupt reserve into "clean" matured PnL and laundering the invariant violation into aggregates. Fix: call validate_reserve_shape(idx) as the first step after the market-mode gate, before any arithmetic. 2) apply_reserve_loss_newest_first did not validate. A malformed queue (horizons out of bounds, sums mismatching reserved_pnl) could be partially consumed and transformed into a different malformed state while returning Ok. Fix: validate_reserve_shape(idx) at entry. 3) advance_profit_warmup validated AFTER the pending→scheduled promotion, so malformed pending fields (e.g., pending_horizon == 0 or out of [h_min, h_max]) were copied into the scheduled bucket before being caught. Moved the validation to the very top; removed the redundant post-promotion check. Regression proofs (reviewer's Tests A, C-variant, D): - rs2_admit_outstanding_rejects_bucket_sum_mismatch - rs3_apply_reserve_loss_rejects_malformed_queue - rs4_warmup_rejects_malformed_pending_before_promotion Not addressed on this pass (not real blockers): - record_uninsured_protocol_loss vault-drain: reviewer was looking at stale code; this is already a no-op (commit 9c0fdde, item 3). - materialize_at O(N): already fixed in commit 498543d via prev_free doubly-linked list. - Slab exhaustion without reclaim path: deployment concern, not an engine bug. reclaim_empty_account_not_atomic is exposed. Verification: - cargo test --features test: all green (165 + 49 + 3 + rest) - 3 new Kani proofs verified individually Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Audit pass found three substance issues in tests I added earlier:
1) ac5_admit_outstanding_atomic_on_err used `if result.is_err() {...}`
which silently passes if result happened to be Ok. Under the test
setup (matured=1, reserve=r, pnl_pos_tot=r → new_matured=1+r>r), the
atomicity check MUST fire, so asserting Err unconditionally is
strictly stronger than the conditional form.
2) fix5_deposit_materialize_requires_min_deposit and
blocker2_deposit_dust_amount_rejected checked `is_err()` only. A bug
in an earlier precondition branch (market_mode, now_slot, vault
overflow) could make the test pass for the wrong reason. Tightened
to assert_eq!(_, Err(RiskError::InsufficientBalance)) and added
post-call !is_used() check where applicable.
3) audit_6_deposit_materialize_needs_live_gate: same — tightened to
Err(Unauthorized) + !is_used verification.
Verification:
- All 9 Kani proofs I added still pass individually (re-run after fix)
- cargo test --features test: 165 unit + 49 default + 3 amm + rest green
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…rpay Two engine correctness fixes surfaced by reviewer pass 3. 1) resolve_market_not_atomic always enforces the deviation band check (previously the "degenerate branch" skipped it). Old discriminator: live_oracle_price == last_oracle_price && rate == 0. This is an accidental value match — a live oracle that happens to be flat is NOT a "dead oracle" signal. When the wrapper passed a matching live_oracle_price, the degenerate branch skipped the band check entirely, and an out-of-band resolved_price (e.g., 40% off with 10% bps limit) was accepted. Fixed: the branch is now purely a "skip accrue" performance optimization. The band check runs unconditionally on both branches. A wrapper needing dead-oracle resolution with an out-of-band price must first widen resolve_price_deviation_bps via governance. Regression test: resolve_market_fresh_same_price_zero_funding_still_ enforces_deviation_band — live = last = 1000, resolved = 1400 (40% off), bps = 10% → MUST reject. Existing k2_resolve_degenerate_bypasses_dt_cap still passes (resolved = live_price → 0% deviation → in-band). 2) deposit_fee_credits rejects amount > outstanding debt. Previously silently capped at `debt`. Since the caller externally moves `amount` tokens before calling this method, booking only `debt` created a real-token ↔ engine.vault divergence. The engine surface now enforces the exact-or-smaller-than-debt contract. Regression tests: - test_deposit_fee_credits_rejects_when_amount_exceeds_outstanding_debt - test_deposit_fee_credits_rejects_when_no_debt_exists - test_deposit_fee_credits_exact_payment_updates_vault_and_insurance_exactly Updated pre-existing test_deposit_fee_credits: its over-payment case asserted silent cap; now expects Err(Overflow) per new contract. Not addressed on this pass: - Claim 1 (wrapper/engine version skew): FALSE — new_account_fee, materialize_with_fee, add_user, add_lp all already removed in item 1 (commit 5666357). Reviewer's wrapper pass reflects the engine state. - Claim 4 (validate_params missing new_account_fee check): FALSE — the field doesn't exist. - Claim 5 (LP fee positive-side accounting): SPEC-DEPENDENT. Current engine only ever decrements fee_credits toward 0 or keeps at 0. If QueryLpFees is an ABI requirement this is a spec gap; otherwise it's unused. Verification: - cargo test --features test: 169 unit + 49 default + 3 amm + rest green - cargo kani --only-codegen: clean - k2_resolve_degenerate_bypasses_dt_cap verified individually Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…+ new_with_market gated Three engine hygiene fixes from reviewer pass 4. 1) free_slot: add capital == 0 and fee_credits == 0 preconditions. Previously only pnl/reserved/basis/bucket-flags were checked, so an upstream bug that left nonzero capital would silently zero it here while c_tot stayed elevated — a real invariant break between account table and aggregates. Similarly fee debt would be silently forgiven. Callers already zero these fields, so this is pure defense-in-depth. 2) init_in_place: fully canonicalize every account field. The method's doc promises "safe even on non-zeroed memory" but the account loop only reset adl_a_basis. Production SBF flow relies on SystemProgram.createAccount zero-init, so in practice this was correct, but an engine method that advertises "canonicalize" must actually canonicalize. The per-field loop is SBF-safe (no stack temporary) and runs once at init; the added write count is negligible. 3) new_with_market: gate behind #[cfg(any(feature = "test", kani))]. The function returns Self by value; on SBF a ~MAX_ACCOUNTS * sizeof(Account) stack object exceeds the 4KB limit. Production callers must use init_in_place on pre-allocated memory. Test and kani callers remain unaffected. `new` was already test-gated. Regression tests (reviewer's exact scenarios): - free_slot_rejects_nonzero_capital - free_slot_rejects_nonzero_fee_credits - init_in_place_fully_canonicalizes_nonzero_memory Not addressed (FALSE claims): - Claim 1 (MAX_PNL_POS_TOT compile overflow): reviewer continues to miscount. Actual literal is 39 digits = 10^38, under u128::MAX ~ 3.4×10^38. cargo check passes. - Claim 2 (resolve degenerate bypass): already fixed in commit 7435d77. Band check now runs unconditionally; discriminator is pure skip-accrue optimization. Verification: - cargo test --features test: 172 unit + 49 default + 3 amm + rest green - cargo kani --only-codegen: clean Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Liveness + performance from the reviewer's follow-up pass: - MAX_TOUCHED_PER_INSTRUCTION: 64 → 256. Counter fields widened u8 → u16. §14's parameter guidance expects 60-220 touches per call under a 1.4M CU budget; the prior 64 cap matched the low end and strangled keeper_crank Phase 2's rr_window_size on large deployments. 256 gives ~4× more Phase 2 touches per call without new state cost beyond the wider counter and the sized array. - InstructionContext.h_max_sticky_accounts[] → h_max_sticky_bitmap[]. Stored as [u64; BITMAP_WORDS] — O(1) test/insert via word-indexed bit ops, replacing the prior O(n) linear scan. Capacity now equals MAX_ACCOUNTS (never exhaustible via distinct-slot marking); the old "sticky full" error branch is unreachable. The ah7_sticky_capacity Kani proof is replaced with ah7_sticky_bitmap_is_idempotent showing mark_h_max_sticky is idempotent and never capacity-bounded. - add_touched: sorted-on-insert (binary search + shift). Preserves the ascending-order invariant that finalize_touched_accounts_post_live relies on, without the prior O(n) linear dedup scan. The explicit insertion-sort pass at finalize-time is now unnecessary and removed. Combined: per-Phase-2-touch cost drops from ~O(n) linear scans (dedup + sticky) to O(log n) + O(n shift) + O(1). At n=256, the shift dominates but is ~4× cheaper than the prior dedup+sticky combo in practice because only one of the two scans is O(n) now. Tests: 240 unit + 3 e2e + 49 lib pass. ah7 Kani proof verifies in 74ms (bitmap semantic check replaces the prior capacity-exhaustion test). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Per reviewer finding #9: `is_terminal_ready` previously short-circuited on `resolved_payout_ready != 0`, trusting the snapshot-ready flag as sufficient evidence of readiness. Under normal invariant history this is correct, but it is not fail-conservative against a corrupt ready flag. Since positive resolved payout is a major safety surface, the function now re-checks all three counters (stored_pos_count, stale_account_count, neg_pnl_account_count) regardless of whether the ready flag is set. A corrupt ready flag alone cannot unlock terminal payout if any counter says otherwise. The ready flag remains a one-way latch for the h_num/h_den payout snapshot, but readiness itself is derived from the counters. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- set_pnl/consume_released_pnl: drop unused new_rel binding, replace with explicit underscored discard on the validation-only subtraction. - enqueue_adl A-truncation: rename a_trunc_rem → _a_trunc_rem (the remainder is unused; we consume only a_candidate_u256). - account_equity_trade_open_raw: idx arg is unused at present; name it _idx to silence the warning until either a caller uses it or we drop it from the signature. - I256::checked_add_i256: the unsigned-overflow flags from the component overflowing_add calls are unused; the sign-based overflow detection below doesn't need them. Renamed to _overflow1/_overflow2. Zero `warning: unused variable` in `cargo build --features test` now. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…itions Three real bugs addressed via TDD (failing tests first, then impl): 1. free_slot head validation (reviewer finding #1) Tests: free_slot_rejects_when_free_head_points_to_used_slot, free_slot_rejects_when_free_head_is_not_head_of_list Fix: Before any mutation, validate free_head is either u16::MAX or a valid in-range free slot with prev_free == u16::MAX. A corrupt in-range head that points at a used slot would graft it into the free list; a corrupt head at a non-head free node would overwrite that node's prev_free pointer. Both now fail conservatively per spec §0 goal 24. 2. enqueue_adl OI_post==0 reset fidelity (reviewer finding #5) Tests: enqueue_adl_sets_both_reset_flags_on_opp_oi_post_zero_symmetric, enqueue_adl_sets_both_reset_flags_on_opp_oi_post_zero_asymmetric Fix: Spec §5.6 step 8 requires BOTH pending-reset flags set unconditionally when OI_post == 0. The prior impl gated the liq_side flag on `self.get_oi_eff(liq_side) == 0`, which matched spec only under valid bilateral symmetry. Under corrupt imbalance the liq_side flag was silently left unset. Now unconditional. 3. assert_public_postconditions cheap O(1) invariants (reviewer #6) Tests: public_postcondition_rejects_matured_exceeding_pos_tot, public_postcondition_rejects_rr_cursor_out_of_range, public_postcondition_rejects_neg_pnl_exceeding_materialized, public_postcondition_rejects_ready_snapshot_with_inverted_ratio Fix: Expand the assertion with five additional cheap global-invariant checks: pnl_matured_pos_tot <= pnl_pos_tot, materialized_account_count <= MAX_MATERIALIZED_ACCOUNTS, neg_pnl_account_count <= materialized_account_count, rr_cursor_position < MAX_MATERIALIZED_ACCOUNTS, and (ready → h_num <= h_den). These catch corruption from internal bugs or direct wrapper writes to public invariant-bearing fields. Also: - Module-level docstring: add ABI-affecting change log for the v2 migration (deposit_fee_credits return type change, top_up_insurance_fund bool → (), six deprecated shims). Tests: 248 unit (242 + 6 new TDD) + 3 e2e + 49 lib = 300 total. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- Delete 7 deprecated pre-v12.19 shims: withdraw_not_atomic, settle_account_not_atomic, execute_trade_not_atomic, liquidate_at_oracle_not_atomic, convert_released_pnl_not_atomic, close_account_not_atomic, keeper_crank_not_atomic (old signature). - Rename each _v2 to the canonical name (no more dual API): withdraw_not_atomic, settle_account_not_atomic, etc. - Each canonical function now takes admit_h_max_consumption_threshold_bps_opt: Option<u128> directly. keeper_crank_not_atomic additionally takes rr_window_size: u64. - Drop the vestigial `_oracle_price` argument from deposit_not_atomic: spec §9.2 deposit does not call accrue_market_to and has no oracle input. Signature is now `(idx, amount, now_slot)`. - Remove `#![allow(deprecated)]` from all test files — nothing deprecated to allow anymore. - Drop the ABI-change log from the module docstring — no migration surface to document. Test call sites (417 deposit calls + 322 live-op calls across 13 test files) mechanically updated: oracle-price arg stripped, trailing `None` / `None, 0` appended where the v12.19 threshold parameter was new. Tests: 248 unit + 3 e2e + 49 lib = 300 total pass. Zero deprecated warnings. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The spec's theoretical 1e6 hard bound and the runtime-configured `params.max_accounts` served no distinct purpose — they both bound the same thing (materialized-account index space). Removing the theoretical bound eliminates: 1. The "dead zone" [params.max_accounts, 1e6) the Phase 2 cursor used to walk before wrapping, which slowed sweep_generation turnover far beyond what the deployment size warranted. 2. The postcondition gap where rr_cursor_position in that dead zone was "valid per spec" but pointed at non-existent slots. 3. Two-bound confusion in docs and tests. Changes: - Delete the MAX_MATERIALIZED_ACCOUNTS constant. - materialize_at cap check: use params.max_accounts. - Phase 2 cursor wrap + postcondition check: use params.max_accounts. - spec.md: replace MAX_MATERIALIZED_ACCOUNTS with cfg_max_accounts (the per-market runtime config field) throughout. - Spec invariant bullet: note that cfg_max_accounts is runtime- configurable rather than a fixed constant. Also adds the cheap postcondition checks the reviewer requested: - num_used_accounts == materialized_account_count - last_oracle_price and fund_px_last are valid oracle-price sentinels - current_slot >= last_market_slot - resolved_payout_ready is a 0/1 latch - Before ready, h_num == h_den == 0 Cleanup: - Drop the stale "Pre-v12.19 shim" doc prefix on keeper_crank_not_atomic. - Correct the withdraw margin comment: Eq_withdraw_raw DOES include haircutted matured PnL (that's the whole point of the withdraw lane vs the trade lane). Tests: 248 unit + 3 e2e + 49 lib = 300 pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reviewer pass addressing items #3, #4, #5, #6: #5: Mode-specific postconditions (spec §2.2 state shape). Live markets must have all resolved_* fields zeroed; Resolved markets must have resolved_price > 0, resolved_live_price > 0, and current_slot == resolved_slot. Failing tests first: public_postcondition_rejects_live_with_nonzero_resolved_price public_postcondition_rejects_live_with_nonzero_resolved_k_delta public_postcondition_rejects_live_with_ready_flag_set public_postcondition_rejects_resolved_with_zero_resolved_price then the check block in assert_public_postconditions. #4: accrue_market_to now calls assert_public_postconditions both at entry (pre-state invariant) and after commit (post-state sanity). The reviewer noted the header promises this for validate-then-mutate public fns but accrue was missing it. With the new oracle-sentinel checks in the postcondition, the pre-call catches a corrupt last_oracle_price == 0 before accrue's price_move_active branch silently skips the cap. #6: keeper_crank_not_atomic now runs assert_public_postconditions at entry too, catching corrupt rr_cursor_position (>= params.max_accounts) or ready-flag inconsistency before any mutation. #3: init_in_place UB boundary stays safe Rust. Added explicit repr- contract docstrings on MarketMode and SideMode documenting that zero-initialized bytes map to a valid discriminant and any non-zero invalid discriminant is the caller's obligation to prevent before forming a &RiskEngine. Moving the storage to u8 would touch ~70 call sites for marginal benefit; the reference-forming boundary is already behind unsafe in practice (SystemProgram zero-inits, Box::new zero-inits). Test updates for stricter postconditions: - Ten test sites that set `market_mode = Resolved; resolved_slot = X; current_slot = resolved_slot;` now also set resolved_price = 1 and resolved_live_price = 1 to maintain Resolved-mode state shape. - test_touch_live_local_does_not_auto_convert: use direct field mutation that keeps aggregate invariants (pnl + pnl_pos_tot + matured match). - reset_leaves_future_mark_headroom: set both long+short OI to preserve bilateral-OI symmetry. proofs_arithmetic.rs: drop the vestigial 4th arg from two deposit_not_atomic call sites that were missed in the earlier sweep (Kani verification runs clean; the build was fine, only Kani found them). Tests: 252 unit + 3 e2e + 49 lib pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Resolved 6 conflict files: - Cargo.toml: combined upstream's small/medium/audit-scan features with fork's [lints.rust] kani cfg. - src/percolator.rs: TAKE_THEIRS — fork's panic-elimination/Result-propagation series (9c40149, 97537c9, e989335, 44d1fe8, ee1ea5f) is subsumed by upstream's broader v12.19 SAFETY cascade. Fork's LIQ_BUDGET_PER_CRANK=24 cap is REAPPLIED in a follow-up commit. - tests/{proofs_instructions,proofs_invariants,proofs_safety,unit_tests}.rs: TAKE_THEIRS — upstream's 2026-04-24 proof-strengthening series rewrites these wholesale. Brings 96 upstream commits (v12.18.x security cascade + v12.19 spec align) into the fork. See /Users/khubair/perc-sync/inventory/CONFLICT_MAP.md (engine section) for full per-conflict resolution rationale. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
📝 WalkthroughWalkthroughThis PR overhauls test/proof harnesses to use admission-based contexts and direct account materialization, updates many test APIs and risk-parameter envelopes for v12.19, adds an Changes
Estimated code review effort🎯 4 (Complex) | ⏱️ ~85 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 unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 9
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (6)
scripts/run_kani_full_audit.sh (1)
43-65:⚠️ Potential issue | 🟡 MinorPer-proof log is deleted even on FAIL/TIMEOUT — keep it for triage.
rm -f "$LOGFILE"runs unconditionally (line 59), so whenever a harness fails or times out you've already echoed only the last 3 lines and then thrown away the full Kani output. For an overnight 20-minute-per-proof audit, retaining the failing/timeout logs is usually worth more than the disk hit.🛠 Suggested change
- tail -3 "$LOGFILE" || true - rm -f "$LOGFILE" + tail -3 "$LOGFILE" || true + if [ "$STATUS" = "PASS" ]; then + rm -f "$LOGFILE" + else + # Preserve failing/timeout logs alongside the TSV for later triage. + mv "$LOGFILE" "/home/anatoly/percolator/kani_audit_${proof}.log" + fi🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@scripts/run_kani_full_audit.sh` around lines 43 - 65, The script currently deletes the per-proof LOGFILE unconditionally, losing full logs for FAIL or TIMEOUT cases; change the cleanup so rm -f "$LOGFILE" only runs for successful proofs (inside the PASS branch) and for FAIL/TIMEOUT preserve the full log (e.g., move or copy "$LOGFILE" to a persistent artifacts directory with a name containing ${proof} and ${STATUS} and echo that path for triage); update the code around LOGFILE, the if that sets STATUS/PASS/FAIL/TIMEOUT, and the tail -3/echo lines to reflect the new flow so failures/timeouts keep their logs while only PASS cases are removed.tests/proofs_invariants.rs (1)
349-381:⚠️ Potential issue | 🟡 Minor
proof_set_pnl_underflow_safetyhas two issues that weaken what it actually tests.
Both
set_pnl_with_reservecalls uselet _ =, but the assertions on lines 368 and 380 require those calls to have succeeded (otherwisepnl_pos_totstays at 0). If a path exists where the admission/reserve call returns Err, the proof's pass/fail signal is ambiguous. Use.unwrap()(or.expect("...")) to fail loudly if the precondition isn't satisfied.
pnl1: u8is fed intoset_pnl_with_reserveas a positivei128(0..255), but the constraint on the second value ispnl2 <= pnl1 as i8. Forpnl1 >= 128,pnl1 as i8reinterprets to a negative value (e.g., 200 → −56), so the "decrease" transition is forced into [−128, −56]. Realistic decrease transitions like 200 → 100 are not covered by this proof. Either boundpnl1: u7/kani::assume(pnl1 < 128), or compare ini128space:kani::assume(pnl2 as i128 <= pnl1 as i128).♻️ Sketch of the fix
- let pnl1: u8 = kani::any(); + let pnl1: u8 = kani::any(); + kani::assume(pnl1 < 128); // keep transitions in non-overflowing signed space let mut ctx = InstructionContext::new_with_admission(0, 100); - let _ = engine.set_pnl_with_reserve( + engine.set_pnl_with_reserve( idx, pnl1 as i128, ReserveMode::UseAdmissionPair(0, 100), Some(&mut ctx), - ); + ).unwrap(); @@ let pnl2: i8 = kani::any(); - kani::assume(pnl2 <= pnl1 as i8); - let _ = engine.set_pnl_with_reserve( + kani::assume((pnl2 as i128) <= (pnl1 as i128)); + engine.set_pnl_with_reserve( idx, pnl2 as i128, ReserveMode::NoPositiveIncreaseAllowed, None, - ); + ).unwrap();🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/proofs_invariants.rs` around lines 349 - 381, The proof proof_set_pnl_underflow_safety is weak because both set_pnl_with_reserve calls ignore errors and pnl1/pnl2 comparison can be invalid due to signed cast wraparound; change the two calls that currently use let _ = engine.set_pnl_with_reserve(...) to unwrap() (or expect) so failures fail the proof, and fix the second-condition by preventing wraparound—either constrain pnl1 to <128 (e.g., kani::assume(pnl1 < 128)) or change the comparison to use the same signed width (e.g., kani::assume(pnl2 as i128 <= pnl1 as i128)) so the decrease transition is correctly represented when updating pnl_pos_tot.tests/proofs_audit.rs (2)
312-364:⚠️ Potential issue | 🟡 MinorProof name
proof_keeper_crank_invalid_partial_no_actionno longer matches the body.The body now only calls
validate_keeper_hint(read-only), notkeeper_crank_not_atomic. Suggest either renaming toproof_validate_keeper_hint_invalid_partial_no_actionor restoring a crank-driven assertion to actually verify "keeper crank performs no liquidation action" rather than just "validation rejects the hint".🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/proofs_audit.rs` around lines 312 - 364, The test named proof_keeper_crank_invalid_partial_no_action no longer invokes keeper_crank_not_atomic and only calls validate_keeper_hint, so either rename the proof to proof_validate_keeper_hint_invalid_partial_no_action or restore a call to keeper_crank_not_atomic and its post-crank assertions; specifically, if you keep the intent of testing the crank, call keeper_crank_not_atomic (or the appropriate engine.keeper_crank_not_atomic wrapper) after validate_keeper_hint and then assert the account's position_basis_q and effective_pos_q remain equal to basis_before and eff_before and that check_conservation() holds; otherwise rename the function to proof_validate_keeper_hint_invalid_partial_no_action to reflect that only validate_keeper_hint is exercised.
113-162:⚠️ Potential issue | 🟠 MajorFIX 2 rollback proofs no longer verify the actual rollback paths in
materialize_at.
add_user_testcallsmaterialize_at, but the test setup (settingnum_used_accounts = MAX_ACCOUNTS) triggers an early bounds check at line 1643–1646 that returns an error beforematerialized_account_countis ever incremented. Consequently, there is no rollback to verify—the counter remains unchanged because it was never modified. The assertionmaterialized_account_count == count_beforepasses trivially.The actual rollback logic in
materialize_at(lines 1654, 1664, 1682, etc.) only executes if the early bounds check passes and the counter has been incremented. The FIX 2 proofs do not exercise these paths. To verify rollback behavior, the test setup should allow the counter to be incremented and then trigger a failure after that point (e.g., bitmap corruption, freelist link corruption).🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/proofs_audit.rs` around lines 113 - 162, The proofs currently set engine.num_used_accounts = MAX_ACCOUNTS which causes an early bounds error before materialize_at increments materialized_account_count, so the rollback paths are never exercised; modify the tests (proof_add_user_count_rollback_on_alloc_failure and proof_add_lp_count_rollback_on_alloc_failure) to allow materialize_at to pass the bounds check (e.g., set engine.num_used_accounts = (MAX_ACCOUNTS as u16) - 1) so materialized_account_count is incremented, then induce a failure after that increment (for example by corrupting the bitmap or freelist state on engine such that materialize_at fails later) and assert that materialized_account_count equals count_before to verify rollback; reference materialize_at, add_user_test, add_lp_test, num_used_accounts, and materialized_account_count when making the changes.tests/proofs_instructions.rs (1)
341-397:⚠️ Potential issue | 🟠 MajorThis proof never reaches the nonzero
fund_termbranch.With
fund_px_last = 100andrate ∈ [-100, 100],fund_num / 1_000_000_000is always0. Theexpected_k_*assertions therefore only check the trivial “no K change” path, so a regression in the payer-driven K/F split would slip through unnoticed.Suggested fix
- let rate: i8 = kani::any(); - kani::assume(rate != 0); - kani::assume(rate >= -100 && rate <= 100); + let rate: i32 = kani::any(); + kani::assume(rate != 0); + kani::assume(rate.unsigned_abs() as u64 <= engine.params.max_abs_funding_e9_per_slot); + kani::assume((100i128 * rate as i128).unsigned_abs() >= 1_000_000_000u128);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/proofs_instructions.rs` around lines 341 - 397, The test never exercises the nonzero fund_term branch because with engine.fund_px_last = 100 and rate constrained to [-100,100], fund_num = 100*rate is always < 1_000_000_000 so fund_term == 0; update the inputs used by accrue_market_to so |fund_num| >= 1_000_000_000 in at least some cases (e.g. set engine.fund_px_last to a much larger value such as 1_000_000_000 or widen the kani::assume range for rate to permit values that produce fund_num ≥ 1_000_000_000 or ≤ -1_000_000_000) so the code paths computing fund_term, expected_k_long/expected_k_short, and the K/F split (used in assertions around expected_k_long, expected_k_short, engine.f_long_num, engine.f_short_num, and the final K+F check) are actually exercised.tests/proofs_v1131.rs (1)
608-666:⚠️ Potential issue | 🟠 MajorThe rejection branch here is unreachable.
now_slotis capped at200, while this harness computesenvelope_topfromlast_market_slot + max_accrual_dt_slots; elsewhere in this filezero_fee_params()is treated as1000, soshould_acceptis always true. That means theelseblock and both rejectioncover!s never execute, so this proof no longer checks the “validate-then-mutate on rejection” behavior it claims to cover.Suggested fix
- let now_slot: u64 = kani::any(); - kani::assume(now_slot >= 50 && now_slot <= 200); - let v_before = engine.vault.get(); let i_before = engine.insurance_fund.balance.get(); let current_before = engine.current_slot; let envelope_top = engine .last_market_slot .checked_add(engine.params.max_accrual_dt_slots) .expect("envelope top"); + let now_slot: u64 = kani::any(); + kani::assume(now_slot >= current_before); + kani::assume(now_slot <= envelope_top.saturating_add(200));🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/proofs_v1131.rs` around lines 608 - 666, The rejection branch is unreachable because now_slot is capped <=200 while envelope_top (engine.last_market_slot + engine.params.max_accrual_dt_slots) can be >200; relax the kani::assume on now_slot so it can exceed envelope_top (e.g., increase the upper bound or constrain using envelope_top so now_slot > envelope_top is possible), ensuring the harness for top_up_insurance_fund(amount, now_slot) can hit the else branch and the is_err() covers; update the assumption near the declaration of now_slot to allow values > engine.last_market_slot + engine.params.max_accrual_dt_slots (envelope_top).
🧹 Nitpick comments (2)
scripts/run_kani_full_audit.sh (1)
36-57: Nit:$FAILconflates failures and timeouts — variable name is misleading.The else-branch unconditionally increments
FAIL(line 56), so on TIMEOUT bothFAILandTIMEOUTSadvance. The summary string at line 75 is correct ("$FAIL failed/timeout ($TIMEOUTS timeout)"), but readers downstream of this script (e.g. anyone parsing intermediate state) will likely expectFAILandTIMEOUTSto be disjoint. Consider either renaming toNONPASS, or makingFAILexclusive by only incrementing it in the inner else.♻️ Optional tweak
else EXIT_CODE=$? if [ $EXIT_CODE -eq 124 ]; then STATUS="TIMEOUT" TIMEOUTS=$((TIMEOUTS + 1)) else STATUS="FAIL" + FAIL=$((FAIL + 1)) fi - FAIL=$((FAIL + 1)) fi…and update the summary to
"$PASS passed, $FAIL failed, $TIMEOUTS timed out, total $TOTAL".🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@scripts/run_kani_full_audit.sh` around lines 36 - 57, The FAIL counter currently increments for both real failures and timeouts, which conflates results; update the loop so FAIL is only incremented when EXIT_CODE is not the timeout code (124) by moving FAIL=$((FAIL + 1)) into the inner else branch that sets STATUS="FAIL", or alternatively rename FAIL to NONPASS and update all usages (including the summary string that currently references "$FAIL failed/timeout ($TIMEOUTS timeout)") to reflect the new name; also consider applying the optional tweak to make the summary explicitly "$PASS passed, $FAIL failed, $TIMEOUTS timed out, total $TOTAL" if you keep the FAIL name.tests/amm_tests.rs (1)
40-67: Consolidate test helpers viamod common;— three redundant copies in amm_tests.rs, fuzzing.rs, and unit_tests.rs.The
add_user_testandadd_lp_testhelpers are defined canonically intests/common/mod.rsbut are redefined identically in three integration test files. Theproofs_*.rstests already usemod common;to access them;amm_tests.rs,fuzzing.rs, andunit_tests.rsshould do the same. This eliminates duplication and reduces the maintenance burden if the engine's materialization protocol changes again.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/amm_tests.rs` around lines 40 - 67, Remove the duplicate helpers add_user_test and add_lp_test from this file and instead import the canonical implementations from the shared test module by adding mod common; at the top and replacing local calls with common::add_user_test and common::add_lp_test (they operate on RiskEngine and call materialize_at; add_lp_test mutates engine.accounts[..].kind to Account::KIND_LP and sets matcher_program/matcher_context), ensuring you delete the local function definitions so the tests use the single source in tests/common/mod.rs.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@kani-list.json`:
- Around line 333-337: The totals.standard-harnesses value in kani-list.json
(totals.standard-harnesses = 305) does not match the PR/audit summary (~287/288
PASS + 1 TIMEOUT); either update totals.standard-harnesses to reflect the actual
run set or add a clarifying note in the audit-results document explaining which
harnesses were excluded and why. Locate the totals object in kani-list.json
(symbol: totals.standard-harnesses) and either correct the count to the audited
harness count or, if the count is intentionally different, add a brief entry in
the audit-results doc referencing the discrepancy and listing the exclusion
criteria or subset used so future readers understand the drift.
In `@src/wide_math.rs`:
- Around line 651-662: The U256 value min_mag is constructed with the 2^127 bit
in the low 128-bit limb (making it 2^127) instead of in the high limb (which
would represent 2^255), so checked_mul_i256 incorrectly rejects valid negative
results; fix by constructing min_mag so its high 128-bit limb equals 1 << 127
and its low limb is 0 (i.e., a U256 whose hi limb has bit 127 set and lo is
zero) and replace the current U256::from_u128(...) expression in
checked_mul_i256 (the block that compares product to min_mag and returns
I256::MIN) with that correct construction so product comparisons reflect 2^255
magnitude.
In `@tests/amm_tests.rs`:
- Around line 200-214: The test advances exactly to the configured boundary by
calling advance_slot(200) then accrue_market_to, which is brittle because 200 ==
max_accrual_dt_slots; change the test to use a safe margin (e.g.
advance_slot(180)) or compute the wait from
default_params().max_accrual_dt_slots minus a small delta and use that value for
advance_slot and the accrue_market_to target so the test stays robust; update
references in this block that call advance_slot(...) and accrue_market_to(...)
accordingly.
In `@tests/common/mod.rs`:
- Around line 128-147: The doc-comment on add_user_test is inaccurate: it claims
the helper "picks the head of the free list and deposits the minimum" but the
function uses the materialize_at back-door (engine.materialize_at) and ignores
the fee argument; update the rustdoc to say this helper allocates a slot by
picking engine.free_head and calling engine.materialize_at(idx,
engine.current_slot) (keeps the unused _fee_payment param for compatibility) and
remove or rephrase references to deposit_not_atomic/deposit paths so readers
won't look for a deposit call that doesn't exist.
- Around line 165-189: The docstring for set_pnl_test claims it uses
"ImmediateRelease otherwise" but the else-branch calls engine.set_pnl which
internally uses ReserveMode::ImmediateReleaseResolvedOnly; update either the doc
or the call to make them consistent: either change the comment to say
"ImmediateReleaseResolvedOnly otherwise" or change the else-branch to call
engine.set_pnl_with_reserve(idx, new_pnl, ReserveMode::ImmediateRelease, None)
(or the exact desired ReserveMode variant) so the code and documentation match;
reference set_pnl_test, engine.set_pnl, set_pnl_with_reserve, and ReserveMode::*
when making the change.
In `@tests/proofs_admission.rs`:
- Around line 835-855: The harness can produce h_min > admit_h_max (10), causing
an invalid admission pair; fix by ensuring the InstructionContext admission max
matches the constraint on h_min: replace the hard-coded 10 in
InstructionContext::new_with_admission_and_threshold(...) with
engine.params.h_max (or alternatively add kani::assume((h_min as u64) <= 10));
this guarantees h_min <= admit_h_max before calling
engine.admit_outstanding_reserve_on_touch and preserves the intended proof
condition checked by assert!(result.is_ok()).
In `@tests/proofs_audit.rs`:
- Around line 813-887: The post-check in the test constructs a cloned post state
but does not deduct the liquidation fee from post.accounts[a].capital, making
post.enforce_partial_liq_post_health(...) overly permissive; update the block
handling Some(LiquidationPolicy::ExactPartial(q)) to compute the liquidation fee
the same way production does and subtract it from post.accounts[a].capital (use
the same fee formula used by the engine's liquidation flow) before calling
post.enforce_partial_liq_post_health; refer to LiquidationPolicy::ExactPartial,
post.accounts[a].capital, account_equity_net, and
enforce_partial_liq_post_health to locate and apply the fee deduction.
In `@tests/proofs_instructions.rs`:
- Around line 2311-2349: The fixture injects capital into engine.accounts[long
as usize].capital and engine.accounts[short as usize].capital without updating
the global totals, breaking conservation; fix by increasing the corresponding
global ledger fields (e.g., engine.c_tot and engine.vault or whichever aggregate
fields track total capital in this engine) by the sum of the injected amounts
(e.g., +200_000) so the global state mirrors the per-account capital before
calling reclaim_empty_account_not_atomic; update the same symbols (engine.c_tot,
engine.vault) used elsewhere in the test harness to preserve invariants.
In `@tests/proofs_invariants.rs`:
- Around line 506-524: The test proof_absorb_protocol_loss_drains_to_zero is
inconsistent with its assertion: update the assertion to match the comment’s
intended behavior after engine.absorb_protocol_loss by checking
insurance_fund.balance is drained to zero when loss >= initial balance,
otherwise equals initial_balance - loss (use
engine.insurance_fund.balance.get(), the local balance variable and the loss
variable to compute the expected value); alternatively, if you prefer to keep
the weaker check, rename the test to
proof_absorb_protocol_loss_never_grows_balance and keep the current <= assertion
to reflect its actual guarantee.
---
Outside diff comments:
In `@scripts/run_kani_full_audit.sh`:
- Around line 43-65: The script currently deletes the per-proof LOGFILE
unconditionally, losing full logs for FAIL or TIMEOUT cases; change the cleanup
so rm -f "$LOGFILE" only runs for successful proofs (inside the PASS branch) and
for FAIL/TIMEOUT preserve the full log (e.g., move or copy "$LOGFILE" to a
persistent artifacts directory with a name containing ${proof} and ${STATUS} and
echo that path for triage); update the code around LOGFILE, the if that sets
STATUS/PASS/FAIL/TIMEOUT, and the tail -3/echo lines to reflect the new flow so
failures/timeouts keep their logs while only PASS cases are removed.
In `@tests/proofs_audit.rs`:
- Around line 312-364: The test named
proof_keeper_crank_invalid_partial_no_action no longer invokes
keeper_crank_not_atomic and only calls validate_keeper_hint, so either rename
the proof to proof_validate_keeper_hint_invalid_partial_no_action or restore a
call to keeper_crank_not_atomic and its post-crank assertions; specifically, if
you keep the intent of testing the crank, call keeper_crank_not_atomic (or the
appropriate engine.keeper_crank_not_atomic wrapper) after validate_keeper_hint
and then assert the account's position_basis_q and effective_pos_q remain equal
to basis_before and eff_before and that check_conservation() holds; otherwise
rename the function to proof_validate_keeper_hint_invalid_partial_no_action to
reflect that only validate_keeper_hint is exercised.
- Around line 113-162: The proofs currently set engine.num_used_accounts =
MAX_ACCOUNTS which causes an early bounds error before materialize_at increments
materialized_account_count, so the rollback paths are never exercised; modify
the tests (proof_add_user_count_rollback_on_alloc_failure and
proof_add_lp_count_rollback_on_alloc_failure) to allow materialize_at to pass
the bounds check (e.g., set engine.num_used_accounts = (MAX_ACCOUNTS as u16) -
1) so materialized_account_count is incremented, then induce a failure after
that increment (for example by corrupting the bitmap or freelist state on engine
such that materialize_at fails later) and assert that materialized_account_count
equals count_before to verify rollback; reference materialize_at, add_user_test,
add_lp_test, num_used_accounts, and materialized_account_count when making the
changes.
In `@tests/proofs_instructions.rs`:
- Around line 341-397: The test never exercises the nonzero fund_term branch
because with engine.fund_px_last = 100 and rate constrained to [-100,100],
fund_num = 100*rate is always < 1_000_000_000 so fund_term == 0; update the
inputs used by accrue_market_to so |fund_num| >= 1_000_000_000 in at least some
cases (e.g. set engine.fund_px_last to a much larger value such as 1_000_000_000
or widen the kani::assume range for rate to permit values that produce fund_num
≥ 1_000_000_000 or ≤ -1_000_000_000) so the code paths computing fund_term,
expected_k_long/expected_k_short, and the K/F split (used in assertions around
expected_k_long, expected_k_short, engine.f_long_num, engine.f_short_num, and
the final K+F check) are actually exercised.
In `@tests/proofs_invariants.rs`:
- Around line 349-381: The proof proof_set_pnl_underflow_safety is weak because
both set_pnl_with_reserve calls ignore errors and pnl1/pnl2 comparison can be
invalid due to signed cast wraparound; change the two calls that currently use
let _ = engine.set_pnl_with_reserve(...) to unwrap() (or expect) so failures
fail the proof, and fix the second-condition by preventing wraparound—either
constrain pnl1 to <128 (e.g., kani::assume(pnl1 < 128)) or change the comparison
to use the same signed width (e.g., kani::assume(pnl2 as i128 <= pnl1 as i128))
so the decrease transition is correctly represented when updating pnl_pos_tot.
In `@tests/proofs_v1131.rs`:
- Around line 608-666: The rejection branch is unreachable because now_slot is
capped <=200 while envelope_top (engine.last_market_slot +
engine.params.max_accrual_dt_slots) can be >200; relax the kani::assume on
now_slot so it can exceed envelope_top (e.g., increase the upper bound or
constrain using envelope_top so now_slot > envelope_top is possible), ensuring
the harness for top_up_insurance_fund(amount, now_slot) can hit the else branch
and the is_err() covers; update the assumption near the declaration of now_slot
to allow values > engine.last_market_slot + engine.params.max_accrual_dt_slots
(envelope_top).
---
Nitpick comments:
In `@scripts/run_kani_full_audit.sh`:
- Around line 36-57: The FAIL counter currently increments for both real
failures and timeouts, which conflates results; update the loop so FAIL is only
incremented when EXIT_CODE is not the timeout code (124) by moving FAIL=$((FAIL
+ 1)) into the inner else branch that sets STATUS="FAIL", or alternatively
rename FAIL to NONPASS and update all usages (including the summary string that
currently references "$FAIL failed/timeout ($TIMEOUTS timeout)") to reflect the
new name; also consider applying the optional tweak to make the summary
explicitly "$PASS passed, $FAIL failed, $TIMEOUTS timed out, total $TOTAL" if
you keep the FAIL name.
In `@tests/amm_tests.rs`:
- Around line 40-67: Remove the duplicate helpers add_user_test and add_lp_test
from this file and instead import the canonical implementations from the shared
test module by adding mod common; at the top and replacing local calls with
common::add_user_test and common::add_lp_test (they operate on RiskEngine and
call materialize_at; add_lp_test mutates engine.accounts[..].kind to
Account::KIND_LP and sets matcher_program/matcher_context), ensuring you delete
the local function definitions so the tests use the single source in
tests/common/mod.rs.
🪄 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: 227d5870-61f0-4f66-83ae-7f93fe45e82f
⛔ Files ignored due to path filters (2)
kani_audit_final.tsvis excluded by!**/*.tsvkani_audit_full.tsvis excluded by!**/*.tsv
📒 Files selected for processing (25)
Cargo.tomlexamples/sizecheck.rsexamples/sizecheck2.rsexamples/sizecheck3.rskani-list.jsonscripts/proof-strength-audit-results.mdscripts/run_kani_full_audit.shspec.mdsrc/percolator.rssrc/wide_math.rstests/amm_tests.rstests/common/mod.rstests/fuzzing.proptest-regressionstests/fuzzing.rstests/proofs_admission.rstests/proofs_arithmetic.rstests/proofs_audit.rstests/proofs_checklist.rstests/proofs_instructions.rstests/proofs_invariants.rstests/proofs_lazy_ak.rstests/proofs_liveness.rstests/proofs_safety.rstests/proofs_v1131.rstests/unit_tests.rs
💤 Files with no reviewable changes (1)
- tests/fuzzing.proptest-regressions
Comment on lines
+333
to
+337
| "totals": { | ||
| "standard-harnesses": 305, | ||
| "contract-harnesses": 0, | ||
| "functions-under-contract": 0 | ||
| } |
There was a problem hiding this comment.
Heads-up: harness count vs. audit summary.
totals.standard-harnesses = 305, but the PR description mentions ≈287/288 PASS + 1 TIMEOUT. If the discrepancy is intentional (e.g., some harnesses excluded from the audit run), consider adding a brief note in the audit-results doc so future readers don't suspect drift between kani-list.json and the run set.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@kani-list.json` around lines 333 - 337, The totals.standard-harnesses value
in kani-list.json (totals.standard-harnesses = 305) does not match the PR/audit
summary (~287/288 PASS + 1 TIMEOUT); either update totals.standard-harnesses to
reflect the actual run set or add a clarifying note in the audit-results
document explaining which harnesses were excluded and why. Locate the totals
object in kani-list.json (symbol: totals.standard-harnesses) and either correct
the count to the audited harness count or, if the count is intentionally
different, add a brief entry in the audit-results doc referencing the
discrepancy and listing the exclusion criteria or subset used so future readers
understand the drift.
Comment on lines
651
to
+662
| // Result must be <= 2^255 (magnitude of MIN) | ||
| // 2^255 as U256: hi limb has bit 127 set (for [u128;2]) or bit 63 of limb[3] (for [u64;4]) | ||
| let min_mag = U256::from_u128(0).checked_add(U256::from_u128(1u128 << 127)).unwrap_or(U256::MAX); | ||
| let min_mag = U256::from_u128(0) | ||
| .checked_add(U256::from_u128(1u128 << 127)) | ||
| .unwrap_or(U256::MAX); | ||
| // For exactly 2^255, result is MIN | ||
| if product == min_mag { return Some(I256::MIN); } | ||
| if product > min_mag { return None; } | ||
| if product == min_mag { | ||
| return Some(I256::MIN); | ||
| } | ||
| if product > min_mag { | ||
| return None; | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Look for any existing Kani/unit coverage that exercises checked_mul_i256
# at magnitudes between 2^127 and 2^255, which would have caught this.
rg -nP --type=rust -C3 'checked_mul_i256'
ast-grep --pattern $'fn checked_mul_i256($_, $_) -> $_ {
$$$
}'Repository: dcccrypto/percolator
Length of output: 3635
🏁 Script executed:
# Read the actual implementation around lines 651-662
sed -n '640,670p' src/wide_math.rsRepository: dcccrypto/percolator
Length of output: 1126
🏁 Script executed:
# Also check the second implementation around lines 876-878
sed -n '866,886p' src/wide_math.rsRepository: dcccrypto/percolator
Length of output: 857
🏁 Script executed:
# Find U256 structure definition to understand limb layout
rg -n 'struct U256|pub struct U256' src/wide_math.rsRepository: dcccrypto/percolator
Length of output: 190
🏁 Script executed:
# Check U256::new() and U256::from_u128() implementations
rg -n -A10 'fn new\(' src/wide_math.rs | head -50Repository: dcccrypto/percolator
Length of output: 669
🏁 Script executed:
# Look for tests of checked_mul_i256
rg -n 'test.*mul_i256|#\[test\]' src/wide_math.rs | head -20Repository: dcccrypto/percolator
Length of output: 404
🏁 Script executed:
# Look for tests specifically for checked_mul_i256 with products near boundaries
rg -n -A20 'fn test.*checked_mul' src/wide_math.rsRepository: dcccrypto/percolator
Length of output: 1059
🏁 Script executed:
# Find I256::MIN definition
rg -n 'MIN.*=' src/wide_math.rs | grep -i i256Repository: dcccrypto/percolator
Length of output: 46
🏁 Script executed:
# Check feature flags to see if there are Kani-specific vs regular implementations
rg -n 'cfg.*kani|#\[cfg' src/wide_math.rs | head -20Repository: dcccrypto/percolator
Length of output: 282
🏁 Script executed:
# Search for tests of checked_mul_i256 with I256 inputs
rg -n -B5 -A15 'checked_mul_i256' src/wide_math.rs | grep -A15 '#\[test\]'Repository: dcccrypto/percolator
Length of output: 46
🏁 Script executed:
# Get I256 definition and constants
rg -n 'pub struct I256|pub const MIN|pub const MAX' src/wide_math.rsRepository: dcccrypto/percolator
Length of output: 805
🏁 Script executed:
# Verify the actual binary representation: what does 2^255 look like in U256?
cat > /tmp/verify_u256.py << 'EOF'
# U256 is [lo, hi] with u128 limbs
# Value = lo + (hi << 128)
# 2^255 in binary: bit 255 is set
# In [lo, hi]: lo = 0, hi = 2^127 (because 2^255 = 2^127 * 2^128)
val_2_255 = 2**255
hi = (val_2_255 >> 128) & ((1 << 128) - 1)
lo = val_2_255 & ((1 << 128) - 1)
print(f"2^255 in U256: lo={lo} ({lo:`#034x`}), hi={hi} ({hi:`#034x`})")
print(f"hi == (1u128 << 127): {hi == (1 << 127)}")
# What does current code compute?
val_current = 1 << 127 # U256::from_u128(1u128 << 127)
print(f"\nCurrent min_mag = 2^127: {val_current} ({val_current:`#034x`})")
print(f"This is 2^{val_current.bit_length() - 1}")
# Example: product = 2^200 should fit in negative I256
val_example = 2**200
print(f"\nExample: product = 2^200")
print(f" Is 2^200 > 2^127? {val_example > (1 << 127)}")
print(f" Is 2^200 < 2^255? {val_example < (1 << 255)}")
print(f" So -2^200 should fit in I256, but code would reject it (None)")
EOF
python3 /tmp/verify_u256.pyRepository: dcccrypto/percolator
Length of output: 486
🏁 Script executed:
# Check if there's any test for I256::checked_mul_i256 at all
rg -n -B2 -A10 'I256.*checked_mul_i256|checked_mul_i256.*I256' src/wide_math.rsRepository: dcccrypto/percolator
Length of output: 1385
min_mag is 2^127, not 2^255 — checked_mul_i256 incorrectly rejects valid negative results.
The calculation U256::from_u128(0).checked_add(U256::from_u128(1u128 << 127)) produces a U256 with [lo=2^127, hi=0], representing the value 2^127. However, I256::MIN = Self([0, 1u128 << 127]) has magnitude 2^255 (since bit 255 is set in two's complement). The intended U256 representation should be [lo=0, hi=2^127], not [lo=2^127, hi=0].
This causes:
- Products in the range
(2^127, 2^255)are wrongly rejected asNone, even though they represent valid negative I256 values. product == 2^127returnsSome(I256::MIN)with incorrect magnitude.- The non-negative path only works by coincidence (
from_u256_or_overflowchecks the hi bit).
The same bug exists in both implementations (Kani at lines 653–655 and non-Kani at lines 876–878). The PR summary states this block was rewritten without changing calculations—confirming the bug is pre-existing but lives on touched lines.
Fix: Replace with correct U256 construction
- let min_mag = U256::from_u128(0)
- .checked_add(U256::from_u128(1u128 << 127))
- .unwrap_or(U256::MAX);
+ let min_mag = U256::new(0, 1u128 << 127);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@src/wide_math.rs` around lines 651 - 662, The U256 value min_mag is
constructed with the 2^127 bit in the low 128-bit limb (making it 2^127) instead
of in the high limb (which would represent 2^255), so checked_mul_i256
incorrectly rejects valid negative results; fix by constructing min_mag so its
high 128-bit limb equals 1 << 127 and its low limb is 0 (i.e., a U256 whose hi
limb has bit 127 set and lo is zero) and replace the current
U256::from_u128(...) expression in checked_mul_i256 (the block that compares
product to min_mag and returns I256::MIN) with that correct construction so
product comparisons reflect 2^255 magnitude.
Comment on lines
200
to
214
| .unwrap(); | ||
| } | ||
|
|
||
| // Advance for full warmup | ||
| engine.advance_slot(200); | ||
| let slot = engine.current_slot; | ||
| { | ||
| let mut ctx = InstructionContext::new_with_h_lock(0); | ||
| let mut ctx = InstructionContext::new_with_admission(0, 100); | ||
| engine.accrue_market_to(slot, new_price, 0).unwrap(); | ||
| engine.current_slot = slot; | ||
| engine.touch_account_live_local(alice as usize, &mut ctx).unwrap(); | ||
| engine | ||
| .touch_account_live_local(alice as usize, &mut ctx) | ||
| .unwrap(); | ||
| engine.finalize_touched_accounts_post_live(&ctx); | ||
| } |
There was a problem hiding this comment.
advance_slot(200) lands exactly on max_accrual_dt_slots.
Phase 4 advances 200 slots and immediately calls accrue_market_to, which is exactly at the configured max_accrual_dt_slots: 200. This passes today but is a fragile boundary — any future tightening (or a non-zero accrual envelope debit before this point) will trip the live-accrual envelope and break this E2E test. Consider giving a small margin (e.g. dt=180) or deriving the wait from default_params().max_accrual_dt_slots.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/amm_tests.rs` around lines 200 - 214, The test advances exactly to the
configured boundary by calling advance_slot(200) then accrue_market_to, which is
brittle because 200 == max_accrual_dt_slots; change the test to use a safe
margin (e.g. advance_slot(180)) or compute the wait from
default_params().max_accrual_dt_slots minus a small delta and use that value for
advance_slot and the accrue_market_to target so the test stays robust; update
references in this block that call advance_slot(...) and accrue_market_to(...)
accordingly.
Comment on lines
+128
to
+147
| /// Test helper: materialize a user account via deposit_not_atomic (spec §10.2). | ||
| /// | ||
| /// v12.18.1 removed add_user / add_lp / materialize_with_fee. The sole | ||
| /// materialization path is deposit with amount >= cfg_min_initial_deposit. | ||
| /// This helper picks the head of the free list and deposits the minimum. | ||
| /// | ||
| /// Accepts an unused `_fee_payment` argument for mechanical migration from the | ||
| /// old `add_user_test(&mut engine, fee)` API; the engine no longer charges a fee. | ||
| pub fn add_user_test(engine: &mut RiskEngine, _fee_payment: u128) -> Result<u16> { | ||
| let idx = engine.free_head; | ||
| if idx == u16::MAX || (idx as usize) >= MAX_ACCOUNTS { | ||
| return Err(RiskError::Overflow); | ||
| } | ||
| // Use materialize_at (test-visible back-door) to allocate a slot without | ||
| // moving capital/vault. The public engine API only materializes via | ||
| // deposit_not_atomic(amount >= min_initial_deposit); that spec-strict | ||
| // path is exercised in dedicated materialization tests. | ||
| engine.materialize_at(idx, engine.current_slot)?; | ||
| Ok(idx) | ||
| } |
There was a problem hiding this comment.
Doc-comment for add_user_test is stale — describes a deposit path, but the code uses the materialize_at back-door.
The header comment states "This helper picks the head of the free list and deposits the minimum.", while the body explicitly bypasses deposit_not_atomic via engine.materialize_at(idx, engine.current_slot). The inline comment on lines 141–144 already says so. Please reconcile the leading rustdoc so future readers don't grep for a deposit that isn't there.
📝 Suggested doc tweak
-/// Test helper: materialize a user account via deposit_not_atomic (spec §10.2).
+/// Test helper: materialize a user account via the test-visible
+/// `materialize_at` back-door (no capital/vault movement).
///
/// v12.18.1 removed add_user / add_lp / materialize_with_fee. The sole
-/// materialization path is deposit with amount >= cfg_min_initial_deposit.
-/// This helper picks the head of the free list and deposits the minimum.
+/// production materialization path is `deposit_not_atomic` with
+/// amount >= cfg_min_initial_deposit; that spec-strict path is
+/// exercised in dedicated materialization tests. This helper instead
+/// allocates the head of the free list directly so PnL/conservation
+/// proofs don't need to model deposit accounting.
///
/// Accepts an unused `_fee_payment` argument for mechanical migration from the
/// old `add_user_test(&mut engine, fee)` API; the engine no longer charges a fee.📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| /// Test helper: materialize a user account via deposit_not_atomic (spec §10.2). | |
| /// | |
| /// v12.18.1 removed add_user / add_lp / materialize_with_fee. The sole | |
| /// materialization path is deposit with amount >= cfg_min_initial_deposit. | |
| /// This helper picks the head of the free list and deposits the minimum. | |
| /// | |
| /// Accepts an unused `_fee_payment` argument for mechanical migration from the | |
| /// old `add_user_test(&mut engine, fee)` API; the engine no longer charges a fee. | |
| pub fn add_user_test(engine: &mut RiskEngine, _fee_payment: u128) -> Result<u16> { | |
| let idx = engine.free_head; | |
| if idx == u16::MAX || (idx as usize) >= MAX_ACCOUNTS { | |
| return Err(RiskError::Overflow); | |
| } | |
| // Use materialize_at (test-visible back-door) to allocate a slot without | |
| // moving capital/vault. The public engine API only materializes via | |
| // deposit_not_atomic(amount >= min_initial_deposit); that spec-strict | |
| // path is exercised in dedicated materialization tests. | |
| engine.materialize_at(idx, engine.current_slot)?; | |
| Ok(idx) | |
| } | |
| /// Test helper: materialize a user account via the test-visible | |
| /// `materialize_at` back-door (no capital/vault movement). | |
| /// | |
| /// v12.18.1 removed add_user / add_lp / materialize_with_fee. The sole | |
| /// production materialization path is `deposit_not_atomic` with | |
| /// amount >= cfg_min_initial_deposit; that spec-strict path is | |
| /// exercised in dedicated materialization tests. This helper instead | |
| /// allocates the head of the free list directly so PnL/conservation | |
| /// proofs don't need to model deposit accounting. | |
| /// | |
| /// Accepts an unused `_fee_payment` argument for mechanical migration from the | |
| /// old `add_user_test(&mut engine, fee)` API; the engine no longer charges a fee. | |
| pub fn add_user_test(engine: &mut RiskEngine, _fee_payment: u128) -> Result<u16> { | |
| let idx = engine.free_head; | |
| if idx == u16::MAX || (idx as usize) >= MAX_ACCOUNTS { | |
| return Err(RiskError::Overflow); | |
| } | |
| // Use materialize_at (test-visible back-door) to allocate a slot without | |
| // moving capital/vault. The public engine API only materializes via | |
| // deposit_not_atomic(amount >= min_initial_deposit); that spec-strict | |
| // path is exercised in dedicated materialization tests. | |
| engine.materialize_at(idx, engine.current_slot)?; | |
| Ok(idx) | |
| } |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/common/mod.rs` around lines 128 - 147, The doc-comment on add_user_test
is inaccurate: it claims the helper "picks the head of the free list and
deposits the minimum" but the function uses the materialize_at back-door
(engine.materialize_at) and ignores the fee argument; update the rustdoc to say
this helper allocates a slot by picking engine.free_head and calling
engine.materialize_at(idx, engine.current_slot) (keeps the unused _fee_payment
param for compatibility) and remove or rephrase references to
deposit_not_atomic/deposit paths so readers won't look for a deposit call that
doesn't exist.
Comment on lines
+165
to
189
| /// Test helper: set PnL to any value, Live-mode compatible. | ||
| /// | ||
| /// `RiskEngine::set_pnl` uses `ImmediateReleaseResolvedOnly` and errs for positive | ||
| /// increases in Live mode. This helper picks the right mode: UseAdmissionPair in | ||
| /// Live (routes positive PnL via admission), ImmediateRelease otherwise. | ||
| pub fn set_pnl_test(engine: &mut RiskEngine, idx: usize, new_pnl: i128) -> Result<()> { | ||
| if new_pnl == i128::MIN { | ||
| return engine.set_pnl(idx, new_pnl); // preserve i128::MIN rejection semantics | ||
| } | ||
| let old_pnl = engine.accounts[idx].pnl; | ||
| let old_pos: u128 = if old_pnl > 0 { old_pnl as u128 } else { 0 }; | ||
| let new_pos: u128 = if new_pnl > 0 { new_pnl as u128 } else { 0 }; | ||
| let h_max = engine.params.h_max; | ||
| if new_pos > old_pos && engine.market_mode == MarketMode::Live { | ||
| let mut ctx = InstructionContext::new_with_admission(0, h_max); | ||
| engine.set_pnl_with_reserve( | ||
| idx, | ||
| new_pnl, | ||
| ReserveMode::UseAdmissionPair(0, h_max), | ||
| Some(&mut ctx), | ||
| ) | ||
| } else { | ||
| engine.set_pnl(idx, new_pnl) | ||
| } | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Confirm the resolved-mode invoked by set_pnl matches the doc claim.
ast-grep --pattern $'pub fn set_pnl(&mut self, $_, $_) -> Result<()> {
$$$
}'
rg -nP --type=rust -C2 'fn set_pnl\b'Repository: dcccrypto/percolator
Length of output: 423
🏁 Script executed:
# Search for i128::MIN usage in the codebase
rg -n 'i128::MIN' --type=rustRepository: dcccrypto/percolator
Length of output: 8592
🏁 Script executed:
# Search for proofs or test references that might use set_pnl_test with edge cases
rg -n 'set_pnl_test' --type=rust -B 3 -A 3Repository: dcccrypto/percolator
Length of output: 4356
🏁 Script executed:
# Check the context around i128::MIN in set_pnl_test to understand the concern
rg -n 'MIN' tests/common/mod.rs -B 2 -A 2Repository: dcccrypto/percolator
Length of output: 417
Update doc comment or call site to align reserve mode naming.
The function doc at line 167–169 states "ImmediateRelease otherwise", but the else-branch (line 182–185) calls engine.set_pnl, which uses ReserveMode::ImmediateReleaseResolvedOnly (confirmed at src/percolator.rs:1918–1920). Either update the doc to reference ImmediateReleaseResolvedOnly or call set_pnl_with_reserve(.., ReserveMode::ImmediateRelease, None) explicitly to match the stated intent.
Regarding i128::MIN rejection: The explicit handling at line 171–172 is sound. Proofs in tests/proofs_invariants.rs consistently exclude i128::MIN via kani::assume, so no proof relies on its specific behavior in set_pnl_test. The rejection semantics are consistent regardless of market mode since the check occurs before any mode-dependent logic.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/common/mod.rs` around lines 165 - 189, The docstring for set_pnl_test
claims it uses "ImmediateRelease otherwise" but the else-branch calls
engine.set_pnl which internally uses ReserveMode::ImmediateReleaseResolvedOnly;
update either the doc or the call to make them consistent: either change the
comment to say "ImmediateReleaseResolvedOnly otherwise" or change the
else-branch to call engine.set_pnl_with_reserve(idx, new_pnl,
ReserveMode::ImmediateRelease, None) (or the exact desired ReserveMode variant)
so the code and documentation match; reference set_pnl_test, engine.set_pnl,
set_pnl_with_reserve, and ReserveMode::* when making the change.
Comment on lines
+835
to
+855
| let h_min: u8 = kani::any(); | ||
| kani::assume(h_min > 0); | ||
| kani::assume((h_min as u64) <= engine.params.h_max); | ||
|
|
||
| engine.vault = U128::new((r as u128) + 100); | ||
| engine.c_tot = U128::new(0); | ||
| engine.accounts[idx].reserved_pnl = r as u128; | ||
| engine.accounts[idx].pnl = r as i128; | ||
| engine.pnl_pos_tot = r as u128; | ||
| engine.accounts[idx].sched_present = 1; | ||
| engine.accounts[idx].sched_remaining_q = r as u128; | ||
| engine.accounts[idx].sched_anchor_q = r as u128; | ||
| engine.accounts[idx].sched_horizon = engine.params.h_max; | ||
|
|
||
| let reserved_before = engine.accounts[idx].reserved_pnl; | ||
| let matured_before = engine.pnl_matured_pos_tot; | ||
| let sched_present_before = engine.accounts[idx].sched_present; | ||
| let ctx = InstructionContext::new_with_admission_and_threshold(h_min as u64, 10, None); | ||
|
|
||
| let result = engine.admit_outstanding_reserve_on_touch(idx, &ctx); | ||
| assert!(result.is_ok(), "valid gated reserve state must not reject"); |
There was a problem hiding this comment.
This harness can construct an invalid admission pair.
h_min is only constrained by engine.params.h_max, but the context is built with admit_h_max = 10. Any h_min > 10 means the proof is calling admit_outstanding_reserve_on_touch with min > max, so assert!(result.is_ok()) stops isolating the nonzero-h_min policy gate.
Suggested fix
- let ctx = InstructionContext::new_with_admission_and_threshold(h_min as u64, 10, None);
+ let ctx = InstructionContext::new_with_admission_and_threshold(
+ h_min as u64,
+ engine.params.h_max,
+ None,
+ );📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| let h_min: u8 = kani::any(); | |
| kani::assume(h_min > 0); | |
| kani::assume((h_min as u64) <= engine.params.h_max); | |
| engine.vault = U128::new((r as u128) + 100); | |
| engine.c_tot = U128::new(0); | |
| engine.accounts[idx].reserved_pnl = r as u128; | |
| engine.accounts[idx].pnl = r as i128; | |
| engine.pnl_pos_tot = r as u128; | |
| engine.accounts[idx].sched_present = 1; | |
| engine.accounts[idx].sched_remaining_q = r as u128; | |
| engine.accounts[idx].sched_anchor_q = r as u128; | |
| engine.accounts[idx].sched_horizon = engine.params.h_max; | |
| let reserved_before = engine.accounts[idx].reserved_pnl; | |
| let matured_before = engine.pnl_matured_pos_tot; | |
| let sched_present_before = engine.accounts[idx].sched_present; | |
| let ctx = InstructionContext::new_with_admission_and_threshold(h_min as u64, 10, None); | |
| let result = engine.admit_outstanding_reserve_on_touch(idx, &ctx); | |
| assert!(result.is_ok(), "valid gated reserve state must not reject"); | |
| let h_min: u8 = kani::any(); | |
| kani::assume(h_min > 0); | |
| kani::assume((h_min as u64) <= engine.params.h_max); | |
| engine.vault = U128::new((r as u128) + 100); | |
| engine.c_tot = U128::new(0); | |
| engine.accounts[idx].reserved_pnl = r as u128; | |
| engine.accounts[idx].pnl = r as i128; | |
| engine.pnl_pos_tot = r as u128; | |
| engine.accounts[idx].sched_present = 1; | |
| engine.accounts[idx].sched_remaining_q = r as u128; | |
| engine.accounts[idx].sched_anchor_q = r as u128; | |
| engine.accounts[idx].sched_horizon = engine.params.h_max; | |
| let reserved_before = engine.accounts[idx].reserved_pnl; | |
| let matured_before = engine.pnl_matured_pos_tot; | |
| let sched_present_before = engine.accounts[idx].sched_present; | |
| let ctx = InstructionContext::new_with_admission_and_threshold( | |
| h_min as u64, | |
| engine.params.h_max, | |
| None, | |
| ); | |
| let result = engine.admit_outstanding_reserve_on_touch(idx, &ctx); | |
| assert!(result.is_ok(), "valid gated reserve state must not reject"); |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/proofs_admission.rs` around lines 835 - 855, The harness can produce
h_min > admit_h_max (10), causing an invalid admission pair; fix by ensuring the
InstructionContext admission max matches the constraint on h_min: replace the
hard-coded 10 in InstructionContext::new_with_admission_and_threshold(...) with
engine.params.h_max (or alternatively add kani::assume((h_min as u64) <= 10));
this guarantees h_min <= admit_h_max before calling
engine.admit_outstanding_reserve_on_touch and preserves the intended proof
condition checked by assert!(result.is_ok()).
Comment on lines
+813
to
887
| /// If validate_keeper_hint approves ExactPartial(q), then the step-14 | ||
| /// post-partial maintenance predicate must also pass on the corresponding | ||
| /// post-partial state. This proves the pre-flight is not over-optimistic | ||
| /// without executing unrelated keeper crank paths. | ||
| #[kani::proof] | ||
| #[kani::unwind(34)] | ||
| #[kani::solver(cadical)] | ||
| fn proof_validate_hint_preflight_conservative() { | ||
| let mut engine = RiskEngine::new(zero_fee_params()); | ||
|
|
||
| let a = engine.add_user(0).unwrap(); | ||
| let b = engine.add_user(0).unwrap(); | ||
| let mut engine = RiskEngine::new_with_market(zero_fee_params(), DEFAULT_SLOT, DEFAULT_ORACLE); | ||
|
|
||
| engine.deposit_not_atomic(a, 1_000_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap(); | ||
| engine.deposit_not_atomic(b, 1_000_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap(); | ||
| let a = add_user_test(&mut engine, 0).unwrap(); | ||
| let b = add_user_test(&mut engine, 0).unwrap(); | ||
|
|
||
| // Open position | ||
| let size = (500 * POS_SCALE) as i128; | ||
| engine.execute_trade_not_atomic(a, b, DEFAULT_ORACLE, DEFAULT_SLOT, size, DEFAULT_ORACLE, 0i128, 0).unwrap(); | ||
|
|
||
| // Inject loss to make a underwater | ||
| engine.set_pnl(a as usize, -800_000i128); | ||
| engine.accounts[a as usize].capital = U128::new(30_000); | ||
| engine.accounts[a as usize].pnl = -20_000; | ||
| engine.c_tot = U128::new(30_000); | ||
| engine.vault = U128::new(30_000); | ||
| engine.neg_pnl_account_count = 1; | ||
| engine.attach_effective_position(a as usize, size).unwrap(); | ||
| engine.attach_effective_position(b as usize, -size).unwrap(); | ||
| engine.oi_eff_long_q = size as u128; | ||
| engine.oi_eff_short_q = size as u128; | ||
| assert!( | ||
| !engine.is_above_maintenance_margin( | ||
| &engine.accounts[a as usize], | ||
| a as usize, | ||
| DEFAULT_ORACLE, | ||
| ), | ||
| "fixture must start below maintenance" | ||
| ); | ||
|
|
||
| // Symbolic q_close_q: 1..499 units (must be < abs(eff)) | ||
| let q_units: u16 = kani::any(); | ||
| kani::assume(q_units >= 1 && q_units <= 499); | ||
| let q_close = (q_units as u128) * POS_SCALE; | ||
|
|
||
| let eff = engine.effective_pos_q(a as usize); | ||
| let hint = Some(LiquidationPolicy::ExactPartial(q_close)); | ||
|
|
||
| let validated = engine.validate_keeper_hint(a, eff, &hint, DEFAULT_ORACLE); | ||
| let validated = engine | ||
| .validate_keeper_hint(a, eff, &hint, DEFAULT_ORACLE) | ||
| .unwrap(); | ||
|
|
||
| // If pre-flight approves ExactPartial, step 14 must also pass | ||
| if let Some(LiquidationPolicy::ExactPartial(q)) = validated { | ||
| assert_eq!(q, q_close, "approved q must match"); | ||
|
|
||
| // Run actual liquidation via keeper_crank_not_atomic | ||
| let slot2 = DEFAULT_SLOT + 1; | ||
| let candidates = [(a, Some(LiquidationPolicy::ExactPartial(q)))]; | ||
| let result = engine.keeper_crank_not_atomic(slot2, DEFAULT_ORACLE, &candidates, 10, 0i128, 0); | ||
|
|
||
| // Crank must succeed (step 14 must pass if pre-flight said OK) | ||
| assert!(result.is_ok(), "keeper_crank_not_atomic must succeed when pre-flight approved ExactPartial"); | ||
|
|
||
| // And the account must still have a position (partial, not converted to full close) | ||
| let eff_after = engine.effective_pos_q(a as usize); | ||
| kani::cover!(eff_after != 0, "partial liquidation preserved nonzero position"); | ||
| let remaining = size - q as i128; | ||
| let mut post = engine.clone(); | ||
| post.attach_effective_position(a as usize, remaining) | ||
| .unwrap(); | ||
| post.attach_effective_position(b as usize, -remaining) | ||
| .unwrap(); | ||
| post.oi_eff_long_q = remaining as u128; | ||
| post.oi_eff_short_q = remaining as u128; | ||
| assert!( | ||
| post.enforce_partial_liq_post_health(a as usize, DEFAULT_ORACLE) | ||
| .is_ok(), | ||
| "approved ExactPartial must satisfy the step-14 post-health check" | ||
| ); | ||
| kani::cover!( | ||
| post.effective_pos_q(a as usize) != 0, | ||
| "partial liquidation preserved nonzero position" | ||
| ); | ||
| } | ||
|
|
||
| // Cover both outcomes | ||
| kani::cover!(matches!(validated, Some(LiquidationPolicy::ExactPartial(_))), "pre-flight approved partial"); | ||
| kani::cover!(matches!(validated, Some(LiquidationPolicy::FullClose)), "pre-flight escalated to full close"); | ||
| kani::cover!( | ||
| matches!(validated, Some(LiquidationPolicy::ExactPartial(_))), | ||
| "pre-flight approved partial" | ||
| ); | ||
| kani::cover!( | ||
| validated.is_none(), | ||
| "pre-flight rejected insufficient partial" | ||
| ); | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Inspect enforce_partial_liq_post_health to determine whether it reads capital/pnl
# and whether step-14 in liquidate_at_oracle_internal applies a fee before calling it.
ast-grep --pattern 'fn enforce_partial_liq_post_health($$$) -> $_ { $$$ }'
echo "---"
rg -nP --type=rust -C5 '\benforce_partial_liq_post_health\b'
echo "---"
rg -nP --type=rust -C2 'liquidation_fee|liq_fee' src/percolator.rs | head -200Repository: dcccrypto/percolator
Length of output: 10387
🏁 Script executed:
# Find is_above_maintenance_margin implementation
rg -nP --type=rust -A15 'fn is_above_maintenance_margin\(' src/Repository: dcccrypto/percolator
Length of output: 930
🏁 Script executed:
# Get full is_above_maintenance_margin implementation
rg -nP --type=rust -A25 'fn is_above_maintenance_margin\(' src/percolator.rsRepository: dcccrypto/percolator
Length of output: 1061
🏁 Script executed:
# Find account_equity_net implementation
rg -nP --type=rust -A10 'fn account_equity_net\(' src/percolator.rsRepository: dcccrypto/percolator
Length of output: 523
🏁 Script executed:
# Find account_equity_maint_raw implementation
rg -nP --type=rust -A10 'fn account_equity_maint_raw\(' src/percolator.rsRepository: dcccrypto/percolator
Length of output: 548
🏁 Script executed:
# Find account_equity_maint_raw_wide implementation
rg -nP --type=rust -A15 'fn account_equity_maint_raw_wide\(' src/percolator.rsRepository: dcccrypto/percolator
Length of output: 910
🏁 Script executed:
# Check if charge_fee_to_insurance modifies account capital/pnl
rg -nP --type=rust -A15 'fn charge_fee_to_insurance\(' src/percolator.rsRepository: dcccrypto/percolator
Length of output: 890
Apply the liquidation fee deduction to the constructed post state before the health check.
The enforce_partial_liq_post_health health check depends on account_equity_net, which reads account.capital. In production (step 10-11), the liquidation fee is charged to capital before step 14 calls enforce_partial_liq_post_health (line 5911, 5951). The test constructs post without deducting this fee from capital, making it artificially healthier than what step 14 actually observes. Subtract the liquidation fee from post.accounts[a].capital before the assertion to match production behavior.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/proofs_audit.rs` around lines 813 - 887, The post-check in the test
constructs a cloned post state but does not deduct the liquidation fee from
post.accounts[a].capital, making post.enforce_partial_liq_post_health(...)
overly permissive; update the block handling
Some(LiquidationPolicy::ExactPartial(q)) to compute the liquidation fee the same
way production does and subtract it from post.accounts[a].capital (use the same
fee formula used by the engine's liquidation flow) before calling
post.enforce_partial_liq_post_health; refer to LiquidationPolicy::ExactPartial,
post.accounts[a].capital, account_equity_net, and
enforce_partial_liq_post_health to locate and apply the fee deduction.
Comment on lines
+2311
to
+2349
| engine.accounts[long as usize].capital = U128::new(100_000); | ||
| engine.accounts[short as usize].capital = U128::new(100_000); | ||
| engine.accounts[long as usize].position_basis_q = POS_SCALE as i128; | ||
| engine.accounts[short as usize].position_basis_q = -(POS_SCALE as i128); | ||
| engine.accounts[long as usize].adl_a_basis = ADL_ONE; | ||
| engine.accounts[short as usize].adl_a_basis = ADL_ONE; | ||
| engine.oi_eff_long_q = POS_SCALE as u128; | ||
| engine.oi_eff_short_q = POS_SCALE as u128; | ||
| engine.stored_pos_count_long = 1; | ||
| engine.stored_pos_count_short = 1; | ||
| assert!(engine.oi_eff_long_q > 0 && engine.oi_eff_short_q > 0); | ||
|
|
||
| // Set account clean (reclaim preconditions). | ||
| engine.accounts[idx as usize].capital = U128::ZERO; | ||
| engine.accounts[idx as usize].pnl = 0; | ||
| engine.accounts[idx as usize].reserved_pnl = 0; | ||
| engine.accounts[idx as usize].position_basis_q = 0; | ||
| engine.accounts[idx as usize].sched_present = 0; | ||
| engine.accounts[idx as usize].pending_present = 0; | ||
| engine.accounts[idx as usize].fee_credits = I128::ZERO; | ||
|
|
||
| // Envelope = last_market_slot + max_accrual_dt_slots. | ||
| let envelope = engine | ||
| .last_market_slot | ||
| .saturating_add(engine.params.max_accrual_dt_slots); | ||
|
|
||
| // Symbolic now_slot beyond envelope but >= current_slot. | ||
| let slack: u8 = kani::any(); | ||
| kani::assume(slack > 0); | ||
| let now_slot = envelope.saturating_add(slack as u64); | ||
| kani::assume(now_slot >= engine.current_slot); | ||
|
|
||
| let current_slot_before = engine.current_slot; | ||
| let used_before = engine.is_used(idx as usize); | ||
| let cap_before = engine.accounts[idx as usize].capital.get(); | ||
| let fee_before = engine.accounts[idx as usize].fee_credits; | ||
|
|
||
| let r = engine.reclaim_empty_account_not_atomic(idx, now_slot); | ||
| assert!( |
There was a problem hiding this comment.
This fixture breaks conservation before reclaim_empty_account_not_atomic() runs.
The harness injects 100_000 of capital into long and short but never mirrors that into c_tot/vault. That means the public entrypoint can reject on the corrupted global state instead of on the envelope violation you’re trying to prove, so the Err(RiskError::Overflow) assertion is not isolating the intended guard.
Suggested fix
engine.accounts[long as usize].capital = U128::new(100_000);
engine.accounts[short as usize].capital = U128::new(100_000);
+ engine.c_tot = U128::new(200_000);
+ engine.vault = U128::new(200_000);
engine.accounts[long as usize].position_basis_q = POS_SCALE as i128;
engine.accounts[short as usize].position_basis_q = -(POS_SCALE as i128);
engine.accounts[long as usize].adl_a_basis = ADL_ONE;
engine.accounts[short as usize].adl_a_basis = ADL_ONE;
engine.oi_eff_long_q = POS_SCALE as u128;
engine.oi_eff_short_q = POS_SCALE as u128;
engine.stored_pos_count_long = 1;
engine.stored_pos_count_short = 1;
+ assert!(engine.check_conservation());📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| engine.accounts[long as usize].capital = U128::new(100_000); | |
| engine.accounts[short as usize].capital = U128::new(100_000); | |
| engine.accounts[long as usize].position_basis_q = POS_SCALE as i128; | |
| engine.accounts[short as usize].position_basis_q = -(POS_SCALE as i128); | |
| engine.accounts[long as usize].adl_a_basis = ADL_ONE; | |
| engine.accounts[short as usize].adl_a_basis = ADL_ONE; | |
| engine.oi_eff_long_q = POS_SCALE as u128; | |
| engine.oi_eff_short_q = POS_SCALE as u128; | |
| engine.stored_pos_count_long = 1; | |
| engine.stored_pos_count_short = 1; | |
| assert!(engine.oi_eff_long_q > 0 && engine.oi_eff_short_q > 0); | |
| // Set account clean (reclaim preconditions). | |
| engine.accounts[idx as usize].capital = U128::ZERO; | |
| engine.accounts[idx as usize].pnl = 0; | |
| engine.accounts[idx as usize].reserved_pnl = 0; | |
| engine.accounts[idx as usize].position_basis_q = 0; | |
| engine.accounts[idx as usize].sched_present = 0; | |
| engine.accounts[idx as usize].pending_present = 0; | |
| engine.accounts[idx as usize].fee_credits = I128::ZERO; | |
| // Envelope = last_market_slot + max_accrual_dt_slots. | |
| let envelope = engine | |
| .last_market_slot | |
| .saturating_add(engine.params.max_accrual_dt_slots); | |
| // Symbolic now_slot beyond envelope but >= current_slot. | |
| let slack: u8 = kani::any(); | |
| kani::assume(slack > 0); | |
| let now_slot = envelope.saturating_add(slack as u64); | |
| kani::assume(now_slot >= engine.current_slot); | |
| let current_slot_before = engine.current_slot; | |
| let used_before = engine.is_used(idx as usize); | |
| let cap_before = engine.accounts[idx as usize].capital.get(); | |
| let fee_before = engine.accounts[idx as usize].fee_credits; | |
| let r = engine.reclaim_empty_account_not_atomic(idx, now_slot); | |
| assert!( | |
| engine.accounts[long as usize].capital = U128::new(100_000); | |
| engine.accounts[short as usize].capital = U128::new(100_000); | |
| engine.c_tot = U128::new(200_000); | |
| engine.vault = U128::new(200_000); | |
| engine.accounts[long as usize].position_basis_q = POS_SCALE as i128; | |
| engine.accounts[short as usize].position_basis_q = -(POS_SCALE as i128); | |
| engine.accounts[long as usize].adl_a_basis = ADL_ONE; | |
| engine.accounts[short as usize].adl_a_basis = ADL_ONE; | |
| engine.oi_eff_long_q = POS_SCALE as u128; | |
| engine.oi_eff_short_q = POS_SCALE as u128; | |
| engine.stored_pos_count_long = 1; | |
| engine.stored_pos_count_short = 1; | |
| assert!(engine.check_conservation()); | |
| // Set account clean (reclaim preconditions). | |
| engine.accounts[idx as usize].capital = U128::ZERO; | |
| engine.accounts[idx as usize].pnl = 0; | |
| engine.accounts[idx as usize].reserved_pnl = 0; | |
| engine.accounts[idx as usize].position_basis_q = 0; | |
| engine.accounts[idx as usize].sched_present = 0; | |
| engine.accounts[idx as usize].pending_present = 0; | |
| engine.accounts[idx as usize].fee_credits = I128::ZERO; | |
| // Envelope = last_market_slot + max_accrual_dt_slots. | |
| let envelope = engine | |
| .last_market_slot | |
| .saturating_add(engine.params.max_accrual_dt_slots); | |
| // Symbolic now_slot beyond envelope but >= current_slot. | |
| let slack: u8 = kani::any(); | |
| kani::assume(slack > 0); | |
| let now_slot = envelope.saturating_add(slack as u64); | |
| kani::assume(now_slot >= engine.current_slot); | |
| let current_slot_before = engine.current_slot; | |
| let used_before = engine.is_used(idx as usize); | |
| let cap_before = engine.accounts[idx as usize].capital.get(); | |
| let fee_before = engine.accounts[idx as usize].fee_credits; | |
| let r = engine.reclaim_empty_account_not_atomic(idx, now_slot); | |
| assert!( |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/proofs_instructions.rs` around lines 2311 - 2349, The fixture injects
capital into engine.accounts[long as usize].capital and engine.accounts[short as
usize].capital without updating the global totals, breaking conservation; fix by
increasing the corresponding global ledger fields (e.g., engine.c_tot and
engine.vault or whichever aggregate fields track total capital in this engine)
by the sum of the injected amounts (e.g., +200_000) so the global state mirrors
the per-account capital before calling reclaim_empty_account_not_atomic; update
the same symbols (engine.c_tot, engine.vault) used elsewhere in the test harness
to preserve invariants.
Comment on lines
506
to
524
| #[kani::unwind(34)] | ||
| #[kani::solver(cadical)] | ||
| fn proof_absorb_protocol_loss_respects_floor() { | ||
| fn proof_absorb_protocol_loss_drains_to_zero() { | ||
| // After the insurance_floor removal, absorb_protocol_loss consumes | ||
| // the full insurance balance. Remaining loss becomes uninsured | ||
| // (handled by the junior haircut mechanism). | ||
| let mut engine = RiskEngine::new(zero_fee_params()); | ||
|
|
||
| let floor: u32 = kani::any(); | ||
| kani::assume(floor <= 10_000); | ||
| engine.params.insurance_floor = U128::new(floor as u128); | ||
|
|
||
| let balance: u32 = kani::any(); | ||
| kani::assume(balance >= floor && balance <= 100_000); | ||
| kani::assume(balance <= 100_000); | ||
| engine.insurance_fund.balance = U128::new(balance as u128); | ||
|
|
||
| let loss: u32 = kani::any(); | ||
| kani::assume(loss > 0 && loss <= 100_000); | ||
| engine.absorb_protocol_loss(loss as u128); | ||
|
|
||
| assert!(engine.insurance_fund.balance.get() >= floor as u128); | ||
| // Balance must never grow from a loss and must not underflow. | ||
| assert!(engine.insurance_fund.balance.get() <= balance as u128); | ||
| } |
There was a problem hiding this comment.
Proof name proof_absorb_protocol_loss_drains_to_zero does not match its assertion.
The body asserts only balance.get() <= balance as u128 (balance never grows). The comment explicitly states post-floor-removal behavior is "consumes the full insurance balance", which would be balance.get() == 0 if loss >= balance else balance - loss. The current assertion is strictly weaker than the documented spec. Either tighten the assertion or rename to something like proof_absorb_protocol_loss_never_grows_balance.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/proofs_invariants.rs` around lines 506 - 524, The test
proof_absorb_protocol_loss_drains_to_zero is inconsistent with its assertion:
update the assertion to match the comment’s intended behavior after
engine.absorb_protocol_loss by checking insurance_fund.balance is drained to
zero when loss >= initial balance, otherwise equals initial_balance - loss (use
engine.insurance_fund.balance.get(), the local balance variable and the loss
variable to compute the expected value); alternatively, if you prefer to keep
the weaker check, rename the test to
proof_absorb_protocol_loss_never_grows_balance and keep the current <= assertion
to reflect its actual guarantee.
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (1)
README.md (1)
170-174: Clarify “extraction-sensitive actions” with explicit examples.This requirement is important, but currently ambiguous for wrapper implementers. Consider naming concrete action classes (e.g., withdrawals, transfer-outs, positive-PnL realization paths) so integrators can enforce it consistently.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@README.md` around lines 170 - 174, Clarify the phrase "extraction-sensitive actions" by listing concrete examples and where wrappers must block or restrict them: explicitly name actions such as withdrawals, transfer-outs, collateral redemptions, debt repayments that lead to net positive-PnL realization, emergency closeouts that transfer funds out, oracle-driven liquidation payouts, and any API endpoints that allow direct fund extraction; update the sentence containing "extraction-sensitive actions" to require wrappers to reject or gate these specific action classes (withdrawals/transfer-outs/positive-PnL realization paths) when raw oracle target and effective engine price diverge, and add a short parenthetical with these examples so integrators have explicit behavior to implement.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@README.md`:
- Around line 14-27: The README mixes version labels (the top section describes
the v12.19 model while later sections still state v12.17); pick a single
canonical version or add a clear “mixed-version” note and then update all
version mentions to match that choice—search for the explicit version strings
"v12.19" and "v12.17" and make them consistent across the document (or insert a
brief note after the "Three Invariants" / "Percolator" headings explaining that
some sections remain at v12.17 and why).
- Around line 118-121: The fenced formula block containing the inequality with
symbols P_new, P_last, max_price_move_bps_per_slot and dt is missing a language
tag; update the opening fence from ``` to a tagged fence such as ```text (or
another appropriate tag) so the block becomes ```text and satisfies markdownlint
MD040 while preserving the formula formatting.
---
Nitpick comments:
In `@README.md`:
- Around line 170-174: Clarify the phrase "extraction-sensitive actions" by
listing concrete examples and where wrappers must block or restrict them:
explicitly name actions such as withdrawals, transfer-outs, collateral
redemptions, debt repayments that lead to net positive-PnL realization,
emergency closeouts that transfer funds out, oracle-driven liquidation payouts,
and any API endpoints that allow direct fund extraction; update the sentence
containing "extraction-sensitive actions" to require wrappers to reject or gate
these specific action classes (withdrawals/transfer-outs/positive-PnL
realization paths) when raw oracle target and effective engine price diverge,
and add a short parenthetical with these examples so integrators have explicit
behavior to implement.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
Comment on lines
+14
to
27
| ## Three Invariants | ||
|
|
||
| A perp exchange has two fairness problems: | ||
| A stressed perp exchange has three jobs: | ||
|
|
||
| 1. **Exit fairness:** when the vault is stressed, who gets paid and how much? | ||
| 2. **Overhang clearing:** when positions go bankrupt, how does the opposing side absorb the residual without deadlocking the market? | ||
| 1. **Backed exits:** when the vault is stressed, nobody can extract more value than the balance sheet can pay. | ||
| 2. **Fair overhang clearing:** when positions go bankrupt, the residual is absorbed pro rata instead of by a discretionary ADL queue. | ||
| 3. **Bounded cranks:** when the oracle moves, the live book is repriced only inside the configured one-step risk budget. | ||
|
|
||
| Percolator solves them with two independent mechanisms that compose cleanly: | ||
| Percolator composes three mechanisms: | ||
|
|
||
| - **H** (the haircut ratio) keeps all exits fair. | ||
| - **A/K** (the lazy side indices) keeps all residual overhang clearing fair, and guarantees markets always return to healthy. | ||
| - **H** (the haircut ratio) makes positive PnL a junior claim on residual value. | ||
| - **A/K/F** (lazy side indices) settles mark moves, funding, and ADL overhang without selecting individual losers. | ||
| - **The price/funding envelope** bounds every exposed accrual step before K/F/price/slot state can mutate. | ||
|
|
There was a problem hiding this comment.
Version signaling is inconsistent with the rest of the document.
Lines 14–27 present the v12.19 model, but later sections still label the feature/spec baseline as v12.17 (e.g., Line 180 and Line 209). For operator and auditor traceability, keep one explicit version target throughout or add a clear “mixed-version” note.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@README.md` around lines 14 - 27, The README mixes version labels (the top
section describes the v12.19 model while later sections still state v12.17);
pick a single canonical version or add a clear “mixed-version” note and then
update all version mentions to match that choice—search for the explicit version
strings "v12.19" and "v12.17" and make them consistent across the document (or
insert a brief note after the "Three Invariants" / "Percolator" headings
explaining that some sections remain at v12.17 and why).
Comment on lines
+118
to
+121
| ``` | ||
| abs(P_new - P_last) * 10_000 | ||
| <= max_price_move_bps_per_slot * dt * P_last | ||
| ``` |
There was a problem hiding this comment.
Add a language tag to the fenced formula block (markdownlint MD040).
Line 118 opens a fence without a language identifier. Please set one (for example text) to satisfy lint and keep formatting consistent.
Suggested patch
-```
+```text
abs(P_new - P_last) * 10_000
<= max_price_move_bps_per_slot * dt * P_last</details>
<!-- suggestion_start -->
<details>
<summary>📝 Committable suggestion</summary>
> ‼️ **IMPORTANT**
> Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
```suggestion
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 118-118: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@README.md` around lines 118 - 121, The fenced formula block containing the
inequality with symbols P_new, P_last, max_price_move_bps_per_slot and dt is
missing a language tag; update the opening fence from ``` to a tagged fence such
as ```text (or another appropriate tag) so the block becomes ```text and
satisfies markdownlint MD040 while preserving the formula formatting.
8 tasks
6 tasks
This was referenced May 10, 2026
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
Engine merge of upstream/master @
3969c31(v12.19 baseline) into fork main9cba53d. Brings 96 upstream commits — 50 SAFETY (Anatoly's "Harden", "Fail closed", "Bound" series), 19 SEMANTIC (v12.18/v12.19 spec bumps), 5 RETIRE (cfg_min_initial_deposit,insurance_floor,_v2/_not_atomicshims), and the omnibusfe1d2d81"v12.19: align spec invariants" (+10405/-7142, 25 files).DO NOT MERGE. This is one half of the perc-sync 2026-04-25 autonomous run. Wrapper-side EXTENSION_PORT merges (landmarks L4/L5) are not yet applied — expect 38 wrapper compile errors against this engine until those land. The PR is here for human review and for traceability of the per-conflict resolutions.
Conflicts resolved (6 files)
Cargo.tomlsmall/medium/audit-scanfeatures with fork's[lints.rust]kani cfgsrc/percolator.rstests/proofs_instructions.rstests/proofs_invariants.rstests/proofs_safety.rstests/unit_tests.rsFork commits subsumed (no follow-up needed)
9c40149,97537c9,e989335,44d1fe8,ee1ea5f9— Result-propagation/panic-elimination, all covered by upstream'sbabfe831/33c2b04f/bc88671e/1299bbdd/9f5ce986/56787463series.Fork commits requiring follow-up
9cba53d(LIQ_BUDGET_PER_CRANK = 24): upstream removed the constant and made it a parameter tokeeper_crank_*. The CU-budget cap (24 liquidations/crank, justified bypercolator-prog/tests/cu_benchmark.rsScenario 9 density sweep) must be re-applied at the wrapper layer. Tracked as a B4 task in the wrapper merge.Build status
cargo build --release --workspace✅ (warnings 31→26, alldead_codefromtest_visible!macros)cargo test --lib --release✅ (49 wide_math tests pass)cargo build --tests --release✅ (integration tests build)max_crank_staleness_slotsremoved,execute_adl_not_atomicrefactored,effective_pos_qprivatized). These are addressed by the wrapper sync L4/L5.slab_types.rs.Recovery
pre-sync-2026-04-25is on origin pointing at9cba53d(annotated tag, append-only).3234d2c.git checkout main && git reset --hard pre-sync-2026-04-25.🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
audit-scanfeature flag to enable additional invariant scanning related to public exits.Tests
Documentation
Chores