sync: adopt v12.17 core engine as canonical main - #87
Merged
Conversation
touch_account_for_liquidation was missing the warmup slope update after mark-to-market settlement. When mark settlement increases AvailGross, spec §5.4 requires w_start_i = current_slot (warmup restart). Without this, stale cap = slope * elapsed allowed premature PnL-to-capital conversion during liquidation. Added Kani proof aeyakovenko#158 (proof_liquidation_must_reset_warmup_on_mark_increase) as regression test. Updated audit results and README: 158 proofs (11 inductive, 145 strong, 2 unit test). Closes #22 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- i5_warmup_bounded_by_pnl: change `||` to `&&` in warmup_cap assertion so the bound is actually verified (was vacuously true due to earlier available-PnL assertion) - i8 equity proofs: clarify comments that account_equity is the realized-only reporting helper, not the margin-check equity per spec §3.3 (margin checks use account_equity_mtm_at_oracle) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adds a new field `fees_earned_total: U128` to the Account struct that tracks cumulative fees generated by LP positions. Updated in execute_trade when fees are charged. This field is read by the rewards program via QueryLpFees to compute LP COIN rewards. Account size grows from 240 to 256 bytes. All tests updated. Also adds .cargo/config.toml with RUST_MIN_STACK=8MB to prevent stack overflow in tests (RiskEngine accounts array is now >1MB). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The proof asserted withdrawal success when equity >= IM and failure when equity < MM, but left the MM <= equity < IM range unchecked. Since withdrawal is risk-increasing, the implementation correctly rejects at IM. Simplified to: equity >= IM → success, equity < IM → failure. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Assert MM < IM in both RiskEngine::new and init_in_place to prevent degenerate margin logic. Updated unit tests that previously used MM == IM or MM == IM == 0 to satisfy the invariant. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace collapsed if/else with explicit checks for all three equity regions: equity >= IM (success), MM <= equity < IM (fail), and equity < MM (fail). Makes the proof's coverage of the IM gap visible. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… resets Complete rewrite of the risk engine to implement the v9.4 specification: - Lazy A/K side indices for ADL (auto-deleveraging) without global scans - i256/u256 wide arithmetic with U512 intermediates for exact mul_div - Fixed-point positions (basis_pos_q: I256, POS_SCALE = 2^64) - Epoch-based lazy settlement with SideMode (Normal/DrainOnly/ResetPending) - Non-compounding quantity basis (same-epoch touches update k_snap only) - Deferred reset finalization via InstructionContext - Precision-exhaustion terminal drain when A_candidate rounds to 0 - absorb_protocol_loss with insurance floor - Warmup restart-on-new-profit with old_warmable capture New files: - src/wide_math.rs: U256, I256, U512, all spec §4.6 helpers (49 tests) Rewritten: - src/percolator.rs: Full v9.4 engine implementation - spec.md: v9.4 specification (source of truth) - tests/unit_tests.rs: 64 unit tests for new API - tests/kani.rs: 41 Kani proofs (6 inductive + 7 bounded + 28 property) - tests/amm_tests.rs: 2 E2E integration tests All 115 tests pass. All 41 Kani proofs verify successfully. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Layered Kani proof suite verifying the lazy A/K mark-to-market, funding, and ADL mechanisms using small-model algebraic proofs (u16/i32 domain with S_POS_SCALE=4, S_ADL_ONE=256) to stay within CBMC solver tractability limits. Tiers: - T0 (4 proofs): Primitive helper correctness (floor_div, mul_div, set_pnl, fee_debt) - T1 (6 proofs): Single-event lazy==eager for mark, funding, ADL quantity/deficit - T2 (3 proofs): Multi-event composition and fold induction - T3 (3 proofs): Epoch mismatch, settle monotonicity, reset counter invariant - T4 (4 proofs): ADL OI balance, A>0 guarantee, drain/bankruptcy routing - T5 (3 proofs): Dust/rounding bounds (quantity error <=1, phantom dust) - T6 (3 proofs): Worked example regressions against production code All 79 harnesses (37 new + 42 existing) pass verification. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Audit findings and fixes: - T0.3-sat: now calls set_pnl and verifies pnl_pos_tot (was: no function call) - T0.4 sat_mul: exercises U256::MAX saturation path (was: u8 only, never saturated) - T0.4 conservation: asserts deposit preserves vault >= c_tot + insurance (was: empty) - T2.12: add floor-shift lemma proof; widen step case k_prefix to full i8 range justified by the lemma (was: bounded to [-15,15]) - T3.14: make position size (u8) and K value (i8) symbolic (was: all concrete) - T3.16: make K value (i8) symbolic (was: all concrete) - T4.17: replace tautology with 2-account OI balance proof via A-shrink and lazy_eff_q (was: asserting x==x) - T5.22: prove 2-account floor-rounding dust sum < 2 units with symbolic positions and A values (was: assert restated assume) - T5.23: prove worst-case dust N*(POS_SCALE-1)/POS_SCALE < N (was: circular) - T6.25: add per-account lazy PnL verification (was: duplicate of T4.19) - T6.26: make K value (i8) and position size (u8) symbolic (was: all concrete) All 80 harnesses (38 ak.rs + 42 kani.rs) pass verification. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Key changes: - Dynamic per-side phantom dust bounds (replaces static MAX_ACCOUNTS cap) - execute_trade explicit post-trade loss settlement for both accounts - keeper_crank must run end-of-instruction reset scheduling/finalization - deposit is pure capital transfer (must not touch positions) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Dynamic phantom dust bounds (per-side counters replacing static MAX_ACCOUNTS cap) - Universal post-trade loss settlement in execute_trade step 11 - InstructionContext + schedule/finalize resets in keeper_crank - Deposit is pure capital transfer (removed touch_account_full) - Skip trivial dust clearance when no dust and no OI exist Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- attach_effective_position: set epoch_snap and k_snap to current side values when zeroing (spec §4.5), matching settle_side_effects - execute_trade: add OI_eff_long == OI_eff_short assertion (step 18) - liquidate_at_oracle: add OI_eff_long == OI_eff_short assertion (step 8) - execute_trade: document step 13 as no-op (no funding-rate input change) - Update module doc version string from v9.4 to v9.5 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Engine fixes (src/percolator.rs): 1. Organic-close bankruptcy bypass — reject undercollateralized flat accounts instead of absorbing losses via resolve_flat_negative 2. Missing reset preflight — add maybe_finalize_ready_reset_sides() auto-finalizing completed resets before side-mode checks 3. Mid-instruction reset in keeper_crank — split liquidate_at_oracle into internal variant, share InstructionContext across crank loop 4. Fee-debt seniority — sweep fee debt immediately after restart conversion yields new capital 5. Warmup restart — capture old_avail before trade, only restart when post-trade availability actually exceeds pre-trade 6. Dust accounting in attach_effective_position — increment phantom dust bound when replacing a basis with nonzero remainder 7. Checked arithmetic — replace saturating/clamping ops with checked variants that panic on corruption in add_u128, sub_u128, mul_u128, update_single_oi, charge_fee_safe, do_profit_conversion, settle_maintenance_fee_internal, fee_debt_sweep Proof suite (tests/ak.rs): - Fix 6 existing broken/weak proofs (T6.24, T4.18, T4.19, T0.4, T0.2, T3.14/T3.16) - Add 26 new proofs across Tiers 7-10: non-compounding basis, dynamic dust/reset lifecycle, ADL fallback branches, engine integration, fee/warmup, accrue_market_to - Total proof count: 65 (up from 39) Test fix (tests/unit_tests.rs): - test_reset_pending_blocks_new_trades: add stale_account_count_short=1 so ResetPending side isn't auto-finalized by new preflight logic Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- t0_2c/t0_2d: increase unwind from 1 to 18 (U512 division loop) - t7_27/t7_28: convert from engine to small-model algebraic proofs (settle_side_effects calls mul_div_floor_u256 → U512 division needs unwind 514+, infeasible for CBMC) - t4_22: convert to small-model (enqueue_adl uses U256 division) - t8_30-t8_34: convert to small-model algebraic proofs (execute_trade and liquidate_at_oracle use U256 division internally) All 65 proofs now pass with their declared unwind bounds. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Addresses gaps identified in proof suite audit: Real-engine proofs with concrete inputs and unwind(70): - T11.39: same_epoch_settle_idempotent — real settle_side_effects path - T11.40: non_compounding_quantity_basis — basis/a_basis unchanged across settles - T11.41: attach_effective_position_remainder — phantom_dust_bound accounting - T11.42: dynamic_dust_bound_inductive — N zeroings → dust_bound >= N - T11.43: end_instruction_auto_finalizes — ResetPending → Normal transition - T11.44: trade_path_reopens_ready_reset — execute_trade auto-finalizes - T11.45: enqueue_adl_nonrepr_beta — beta overflow → absorb, A still shrinks - T11.46: enqueue_adl_k_add_overflow — K overflow → absorb, A still shrinks - T11.47: precision_exhaustion_terminal_drain — A_candidate=0 → both resets - T11.48: bankruptcy_routes_q_D_zero — D=0 → K unchanged, A shrinks - T11.49: pure_pnl_bankruptcy — q_close=0, D>0 → K changes, A unchanged - T11.50: execute_trade_atomic_oi_sign_flip — position flip preserves OI balance - T11.51: execute_trade_slippage_zero_sum — zero-fee trade preserves vault - T11.52: touch_account_full_restart_fee_seniority — warmup + fee debt sweep - T11.53: keeper_crank_quiesces — early break on pending_reset - T11.54: worked_example_regression — open, ADL, settle with final assertions Total proof count: 81 (up from 65). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ero k_diff - t5_23: rewrite from static account-count dust bound to dynamic phantom_dust_bound model matching current engine design - t6_26b: full drain reset regression with nonzero k_diff (the hard path) — terminal K_epoch_start used, nonzero pnl_delta realized, stale counters decrement, basis zeroes, reset finalizes safely Total proof count: 82. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1. enqueue_adl signed representability: replace broken from_raw_u256_pub(x).checked_neg() with try_negate_u256_to_i256() that correctly rejects magnitudes > 2^255 (critical: old code could turn bankruptcy loss into gain for large D values) 2. Side-mode gating: check_side_mode_for_trade now gates on net side OI increase across both trade accounts, not per-account position increase (was too restrictive, blocking valid OI-neutral trades) 3. Fee-credit invariants: deposit_fee_credits rejects amount > i128::MAX (was silently wrapping via u128 as i128); settle_maintenance_fee and fee_debt_sweep use saturating_sub/add instead of unwrap_or silent clamps that could forgive debt or lose precision 4. enqueue_adl liq-side OI: saturating_sub → checked_sub returning Err(CorruptState) on underflow Proof suite: t11_45 rewritten as algebraic try_negate_u256 correctness proof; t11_46/48/49 use POS_SCALE instead of ADL_ONE to keep U512 division shift within unwind(70); kani.rs side-mode proof fixed with stale_account_count. All 82 proofs + 64 unit tests passing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The floor in A_candidate = floor(A_old * OI_post / OI) injects up to
ceil(OI / A_old) q-units of phantom OI into the authoritative OI_eff
tracker. When all opposing users close their positions, this untracked
dust remains in OI_eff. schedule_end_of_instruction_resets then fails
with CorruptState (OI_eff > phantom_dust_bound), permanently deadlocking
the market — no user can ever close their final position.
Fix: after computing A_candidate, add ceil(OI / A_old) to
phantom_dust_bound_opp_q. This is economically microscopic (≤ 2^40
internal q-units ≈ 2^{-24} base tokens in the worst case) but
mathematically guarantees that legitimate clean-empty states always
pass the strict clear_bound_q check.
Proof-driven: t12_53 written first, confirmed the deadlock via Kani
(schedule_end_of_instruction_resets returned Err(CorruptState) with
truncation dust ≈ 0.429 * POS_SCALE vs phantom_dust_bound = 1).
After fix, proof passes. All 83 proofs + 64 unit tests verified.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Updates §5.6 step 8, pseudocode, invariant 5, invariant 28, and key changes to document that enqueue_adl must add ceil(OI / A_old) to phantom_dust_bound_opp_q after floor-truncating A_candidate. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… fee seniority - Payer-driven funding rounding (§5.4): ceil for payer, floor for receiver - Fused delta_K_abs = ceil(D*A*POS_SCALE/OI) in enqueue_adl (§5.6) - Conditional A-truncation dust only when remainder != 0 (§5.6) - stored_pos_count_opp == 0 early return with absorb_protocol_loss (§5.6) - Bilateral/unilateral split in schedule_end_of_instruction_resets (§5.7) - inc_phantom_dust_bound_by helper (§4.6.1) - mul_div_floor_u256_with_rem helper for A_candidate remainder - Immediate fee sweep after restart_on_new_profit in execute_trade (§6.5) - 7 new kani proofs (T13.54-T13.60) for v10.5 coverage - 1 new unit test for spec property #23 (fee seniority) - Updated all affected kani proofs for fused delta_K formula Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1. Replace t7_28 with two correct theorems:
- t7_28a: correct floor inequality direction
(total_two_touch <= pnl_single, not >=)
- t7_28b: exact additivity for divisible K increments
2. Strengthen t11_52 (fee seniority):
- Assert on fee_credits, capital, and insurance fund
- Not just k_snap update
3. Strengthen t11_53 (crank quiescence):
- Use 3 accounts instead of 2
- Verify 3rd account's state is completely unchanged
after pending reset triggers on 2nd
4. Add Tier 14 inductive dust-bound proofs (T14.61-T14.65):
- T14.61: ADL A-truncation formula sufficient (2 accounts, symbolic)
- T14.62: Same-epoch position zeroing preservation
- T14.63: Position reattach remainder preservation
- T14.64: Full-drain reset trivial preservation
- T14.65: End-to-end engine clearance (ADL → close → reset)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…panic 1. CRITICAL: keeper_crank now propagates errors from touch_account_full and liquidate_at_oracle_internal instead of swallowing them. Prevents committing half-mutated state after internal failures. 2. HIGH: enqueue_adl uses checked_mul_div_ceil_u256 for delta_K_abs. If quotient overflows U256 (extreme D/OI ratio), routes to absorb_protocol_loss instead of panicking (§1.5 Rule 14). 3. HIGH: settle_maintenance_fee_internal clamps fee_credits to -(i128::MAX) instead of allowing i128::MIN, which is a dangerous sentinel value for downstream negation operations. 4. HIGH: charge_fee_safe clamps PnL on underflow instead of panicking. Prevents bricking liquidations for deeply underwater accounts (§1.5 Rule 16). 5. MINOR: checked_u256_mul_i256 uses try_negate_u256_to_i256 for the negative path, correctly handling the product == 2^255 boundary (I256::MIN) instead of returning a false overflow. Issue #3 from audit (funding ceil vs floor) is NOT a bug — spec §5.4 step 5 explicitly mandates ceil for payer K-space loss. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… tautology removal - t13_54: replace false raw-sum no-mint assertion (dk_long + dk_short <= 0) with correct cross-multiplied form (dk_long*A_short + dk_short*A_long <= 0) - t11_53: rewrite crank quiescence test to trigger pending_reset via liquidation → enqueue_adl (dust clearance runs post-loop, not mid-loop) - ADL small models (t1_8, t1_8b, t1_9, t4_19, t6_24, t6_25, t13_59): remove extra S_POS_SCALE from delta_k_abs — POS_SCALE cancels with OI_eff denominator (OI_eff = OI_base * POS_SCALE) - t6_24: update hardcoded values (delta_k 256→64, K 2304→2496, PnL 72→78) - Tier 8 (t8_30-34): delete tautological proofs that proved algebraic identities about local variables without exercising engine code Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ot mark 1. schedule_end_of_instruction_resets: propagate errors with ? in all 5 call sites (withdraw, execute_trade, liquidate_at_oracle, keeper_crank, close_account) instead of discarding with let _ 2. execute_trade: reject a == b self-trades — prevents one account from creating matched OI on both sides with only one stored position 3. accrue_market_to: apply mark-only delta_P when dt == 0 but price changed — previously silently dropped same-slot price moves 4. add_user/add_lp c_tot: replace saturating_add with checked_add, return Err(Overflow) on violation. settle_maintenance_fee_internal: return Result<()>, use checked arithmetic instead of saturating/clamping 5. charge_fee_safe: return Result<()> with checked_sub instead of clamping — propagates error to callers instead of silently absorbing Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… compile - t1_8/t1_9: add upper bound assertion (lazy_loss <= eager_loss + q_base) - t11_52: set pre-existing positive PnL so restart_on_new_profit converts warmable → capital via do_profit_conversion (old_warmable > 0) - t13_54: replace I256::checked_mul (doesn't exist) with i128 arithmetic Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…acle touch_account_full mutates state (PnL settle, fee sweep, position zeroing) even when liquidation returns Ok(false). Skipping schedule/finalize resets on that path could leave a clean-empty market stuck in Normal mode instead of entering ResetPending for garbage collection. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Decompose 132 proofs from 2 monolithic files (kani.rs, ak.rs) into 6 topic-based files matching the 7-section proof checklist: - proofs_arithmetic.rs (16 proofs) — pure math helper correctness - proofs_invariants.rs (26 proofs) — global inductive invariants - proofs_lazy_ak.rs (28 proofs) — A/K refinement, events, settlement - proofs_safety.rs (27 proofs) — economic safety, conservation - proofs_instructions.rs (32 proofs) — per-instruction correctness - proofs_liveness.rs (9 proofs) — liveness, progress, no-deadlock Add tests/common/mod.rs with shared helpers, constants, and small-model functions. Add 6 new Kani proofs covering gaps in the checklist. Add 20 new unit tests covering CBMC-impractical gaps: wide arithmetic (U512 paths), multi-step funding accrual, keeper crank behavior, liquidation lifecycle, conservation full-lifecycle, oracle boundaries, maintenance fee overflow, PnL boundary safety, and side-mode gating. All 138 Kani proofs compile-check. All 91 unit tests pass. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- OI symmetry asserts in settle/trade/liquidation/keeper -> Err(CorruptState) - consume_released_pnl: returns Result<()>, all asserts -> checked returns - finalize_touched_accounts_post_live: returns Result<()> - settle_losses / resolve_flat_negative: i128::MIN guards -> early return - Remaining assert! in consume_released_pnl matured invariant Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1. Resolved reconciliation uses compute_kf_pnl_delta_wide() which accepts I256 k_now/f_now — terminal K sum no longer narrowed to i128 before settlement. Fixes false-overflow near K headroom. 2. Same-epoch resolved accounts are handled correctly (side was already ResetPending before resolution). Stale accounts use wide terminal K. 3. set_pnl_with_reserve: UseHLock validity (live mode, h_lock bounds) now pre-validated before any persistent mutation, not just NoPositiveIncreaseAllowed. 4. advance_profit_warmup: corrupt bucket metadata (present flags with zero reserve) handled conservatively instead of asserting. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…lpers - effective_pos_q: assert on overflow -> return 0 (unreachable under bounds) - set_position_basis_q: side count checked_sub/add -> saturating (internal) - set_pnl: internal wrapper uses let _ = instead of expect (callers validate) - Remaining asserts are in internal helpers with caller-validated inputs, constructor-only validate_params, or arithmetic bounded by MAX_VAULT_TVL Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1. keeper_crank: removed eager fee_debt_sweep from candidate loop. Fee sweep deferred to finalize_touched_accounts_post_live, eliminating instruction-order-dependent insurance draw before bankruptcy ADL. 2. reconcile_resolved: same-epoch nonzero basis in resolved mode now returns Err(CorruptState). After resolution, all nonzero-basis accounts must be stale (epoch mismatch). 3. settle_losses: returns Result<()>, Err(CorruptState) on i128::MIN. 4. resolve_flat_negative: returns Result<()>, Err on i128::MIN. 5. advance_profit_warmup: ghost bucket flags defensively cleared. 6. Tests: resolved-close tests updated to use proper resolve_market_not_atomic lifecycle instead of direct MarketMode::Resolved assignment. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…allible 1. set_pnl: returns Result<()> instead of swallowing errors with let _ = 2. settle_losses / resolve_flat_negative: all callers now propagate ? in touch_account_live_local, execute_trade, deposit, reconcile paths 3. set_position_basis_q: checked_sub/add with expect (internal helper, callers validate; previously saturating which hid corruption) 4. advance_profit_warmup: returns Result<()>. Ghost bucket flags -> Err. Post-warmup invariant checks -> Err instead of assert. 5. keeper_crank OI symmetry assert -> Err(CorruptState) 6. deposit: settle_losses error now propagated (was dropped) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…e-open strict 1. deposit: pre-validates PNL != i128::MIN before any mutation, maintaining validate-then-mutate contract for non-_not_atomic entrypoint 2. advance_profit_warmup: fails closed on all corrupt bucket states: - R>0 with no buckets -> Err(CorruptState) - sched_horizon==0 -> Err(CorruptState) (not silent full maturity) - sched_start_slot in future -> Err(CorruptState) (not saturating_sub) - sched_total < sched_release_q -> Err(CorruptState) - pnl_matured_pos_tot overflow -> Err(Overflow) 3. stale-counter in live settlement: checked_sub with Err(CorruptState) instead of saturating_sub(1) that hid underflow 4. account_equity_trade_open_raw: corrupt aggregates -> i128::MIN+1 (blocks all trades) instead of unwrap_or fallbacks that could admit them Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1. deposit renamed to deposit_not_atomic: honestly reflects that settle_losses can Err after state mutation (SVM rollback protects storage, but naming contract is now accurate) 2. set_pnl_with_reserve: old_pos - reserved_pnl -> checked_sub with Err 3. consume_released_pnl: all reserve subtractions -> checked_sub with Err 4. set_position_basis_q: MAX_ACTIVE_POSITIONS_PER_SIDE overflow handled with rollback instead of assert Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…_atomic Reset core engine to toly's upstream/master (719c408) which brings: - v12.17 two-bucket warmup (replaces 62-cohort queue) - Per-side cumulative funding (f_long_num/f_short_num + f_snap) - ADL precision raised (ADL_ONE 1e15, MIN_A_SIDE 1e14) - MAX_ACCOUNTS 4096, panic→Result hardening throughout - ResolvedCloseResult enum, new public APIs Re-added on top: - small/medium feature flags for MAX_ACCOUNTS (256/1024) for rent savings - execute_adl_not_atomic ported to v12.17 API signatures Dropped: entry_price (computed off-chain from position_basis_q / effective_pos_q) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1. set_position_basis_q: returns Result<()>. Side-count overflow returns Err(Overflow) instead of broken silent rollback. All checked_sub/add use ok_or(CorruptState). 2. attach_effective_position: returns Result<()>. MAX_POSITION_ABS_Q and side_of_i128 now return Err instead of panic. 3. append_or_route_new_reserve: returns Result<()>. Reserve/anchor overflow uses ok_or(Overflow). 4. set_pnl_with_reserve decrease branch: remaining asserts on bucket flags and matured invariant converted to Err(CorruptState). 5. consume_released_pnl: matured invariant assert -> Err. 6. touch_account_live_local: Live mode assert -> Err(Unauthorized). 7. liquidate: i128::MIN assert -> Err(CorruptState). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ult checked 1. advance_profit_warmup: bucket-total consistency check at entry (sched_remaining + pending_remaining must equal reserved_pnl). reserved_pnl -= release now uses checked_sub. 2. set_capital: returns Result<()>, c_tot overflow/underflow -> Err 3. fee_debt_sweep: returns Result<()>, all expects -> ok_or 4. inc_phantom_dust_bound/_by: returns Result<()>, expects -> ok_or 5. withdraw vault subtraction: checked_sub instead of sub_u128 6. Header updated to reflect deposit_not_atomic rename Remaining 22 expects are in: add_u128/sub_u128 (MAX_VAULT_TVL bounded), alloc_slot (pre-validated capacity), I256 arithmetic (256-bit, impossible). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…8 removal
1. validate_reserve_shape(): comprehensive per-bucket coherence check:
- absent bucket => all fields zero
- present scheduled => horizon > 0, release <= anchor, remaining <= anchor
- total: sched_remaining + pending_remaining == reserved_pnl
Called at entry and exit of advance_profit_warmup.
2. Fixed missed ? propagations:
- settle_side_effects_with_h_lock: inc_phantom_dust_bound(side)?
- withdraw_not_atomic: set_capital(...)?
3. Replaced all add_u128 calls in state-mutating paths with checked_add:
- deposit_not_atomic, finalize_touched, convert_released_pnl,
close_resolved_terminal — all use .checked_add().ok_or(Overflow)?
- add_u128() now has zero callers (dead code)
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…in ADL execute_adl_not_atomic had two dropped Result returns: - attach_effective_position(target_idx, 0) at step 7 (line 4537) - set_capital(target_idx, new_cap) at step 10 (line 4559) If either fails, the error was silently discarded, leaving OI counts and c_tot desynced from actual account state. Add ? to both calls.
set_capital returns Result<()> since 305ce28 but withdraw_not_atomic at line 3121 dropped the Result without ?. If c_tot was already desynced by a prior bug, the corruption would propagate silently. This bug also exists in upstream (aeyakovenko/percolator@305ce28).
- inc_phantom_dust_bound: propagate Result at line 1623 (was silently dropped while the companion call at line 1249 correctly used ?) - alloc_slot: .expect() → .ok_or(RiskError::CorruptState)? at line 852 - materialize_at: same change at line 949 All remaining expect() calls are now in I256 arithmetic (256-bit, structurally impossible to overflow) or add_u128/sub_u128 (bounded by MAX_VAULT_TVL). These are intentionally kept per upstream design.
Last caller of the panicking add_u128 helper was in execute_adl_not_atomic (fork-specific code not covered by upstream's 57b5c00 cleanup). Replaced with inline checked_add().ok_or(RiskError::Overflow)?. Removed both add_u128 and sub_u128 definitions — zero callers remain.
1. Added .unwrap() to 20 set_capital/set_position_basis_q/fee_debt_sweep calls across 5 proof files — these functions now return Result<()> but the proofs were silently dropping the Result. 2. Added 3 new ADL proofs (fork-specific execute_adl_not_atomic): - proof_adl_preserves_c_tot_invariant: c_tot == sum(capitals) after ADL - proof_adl_preserves_oi_balance: oi_eff_long == oi_eff_short after ADL - proof_adl_zeroes_target_position: position == 0 on successful ADL These proofs cover the F-1 and F-3 bug class: if attach_effective_position or set_capital errors were silently dropped, Kani would detect the invariant violation.
Remove NOT PRODUCTION READY disclaimer. Add features list (v12.17 two-bucket warmup, per-side funding, ADL), build/test commands, Kani proof instructions, links to spec.md and THREAT_MODEL.md. Create THREAT_MODEL.md covering trust assumptions (admin, oracle, keeper, matcher), 5 deferred findings (F-6, C-7, C-12, SP-2, SP-5), deployment checklist, program IDs, and audit status summary. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Mark F-6 and SP-2 as resolved/fixed (see percolator-prog 4fe485a / prior). C-7 and C-12 explicitly tagged ACCEPTED RISK with monitoring plan. SP-5 clarified as governance policy (no on-chain setter exists today). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The MTM-margin-check liquidation path (insurance-funded, not force-realize) costs ~26K CU per liquidation on top of a ~513K base scan. At 24 liqs a crank consumes ~1.18M CU (84.5% of Solana's 1.4M tx budget); at 32 liqs it reliably exceeds the budget and the runtime rejects the tx. Measured via percolator-prog/tests/cu_benchmark.rs Scenario 9 density sweep. Force-realize path is unaffected (502K CU at 4095 users, well under budget). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The v12.17 upstream sync (session 2026-04-15 v2) was done on laptop but never pushed to origin. Meanwhile PR #85 (Kani resurrect) and PR #86 (threat model port) were merged against the stale v12.1.0 main, creating a mismatch with percolator-prog and SDK beta.34 which both expect v12.17. This merge restores consistency: - Core engine now at v12.17.0 (ADL_ONE=1e15, MIN_A_SIDE=1e14, f_snap, two-bucket warmup, no entry_price/account_id) - 457 proofs in tests/proofs_*.rs (replaces 349 v12.1-adapted proofs in tests/kani.rs that had 18 spec-behavior FAILs) - THREAT_MODEL.md preserved (identical file) - LIQ_BUDGET_PER_CRANK = 24 (today's fix to fit 1.4M CU budget) The prior main state (v12.1.0 + PR #85 + PR #86) is preserved on branch 'archive/v12.1-pre-sync' for reference. Using git merge -s ours to keep laptop's tree verbatim; main's tree content is intentionally dropped. See decision_freeze_engine_at_v12_15.md in session memory for the reasoning behind the v12.17 decision.
|
Caution Review failedThe pull request is closed. ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (31)
📝 WalkthroughWalkthroughThis PR consolidates testing infrastructure, removes CI workflows, simplifies numeric operations in I128, adds checked arithmetic APIs to I256, introduces offset-checking examples, and performs extensive refactoring of test/proof suites with updated API signatures and parameter structures. Changes
Sequence Diagram(s)(No sequence diagrams generated—changes are primarily test refactoring, configuration removal, and API signature updates without introducing new multi-component control flows or feature interactions that would benefit from visualization.) Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Poem
✨ Finishing Touches📝 Generate docstrings
🧪 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 |
This was referenced May 9, 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
Promotes the laptop's v12.17 core engine to main, restoring consistency with
percolator-progand SDK beta.34 which both already expect v12.17 semantics.Why
The v12.17 upstream sync was completed on 2026-04-15 (memory: session_2026_04_15_v2_summary.md) but never pushed to origin. Meanwhile:
percolator-progon origin/main references v12.17 engine constants viapath = "../percolator"— cannot compile against origin/main.@percolatorct/sdk@1.0.0-beta.34hardcodes v12.17 layout (V12_17_ACCOUNT_SIZE = 368, two-bucket warmup decoders).The whole ecosystem already expects v12.17; only this repo's main was behind.
Engine version markers
Included
Mechanics
git merge -s oursto keep laptop tree while including main as second parent. Admin-merge required (same pattern as PR #85).Safety
Current main archived to
archive/v12.1-pre-sync(03a0509) — nothing lost.Verification
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Tests
Documentation
Removals
Build Changes