2929//! Internal helpers (`enqueue_adl`, `liquidate_at_oracle_internal`, etc.)
3030//! are not individually atomic — they rely on the calling `_not_atomic`
3131//! method to propagate `Err` to the transaction boundary.
32+ //!
33+ //! # ABI-affecting changes across v12.19 `_v2` introduction
34+ //!
35+ //! - Six live-op shims (`withdraw_not_atomic`, `settle_account_not_atomic`,
36+ //! `execute_trade_not_atomic`, `liquidate_at_oracle_not_atomic`,
37+ //! `convert_released_pnl_not_atomic`, `close_account_not_atomic`) are
38+ //! `#[deprecated]`. Each has a `_v2` counterpart that accepts an
39+ //! `admit_h_max_consumption_threshold_bps_opt: Option<u128>` parameter
40+ //! per spec §4.7 step 2. Shim forwarding passes `None`; trusted/private
41+ //! wrappers may continue using the shims under spec §12.21's explicit
42+ //! carve-out.
43+ //! - `keeper_crank_not_atomic` is similarly deprecated in favor of
44+ //! `keeper_crank_not_atomic_v2` which additionally accepts a
45+ //! `rr_window_size: u64` for Phase 2 structural sweep width.
46+ //! - `deposit_fee_credits` return type: `Result<()>` → `Result<u128>`.
47+ //! Returns `pay = min(amount, FeeDebt_i)` per spec §9.2.1 step 5. The
48+ //! wrapper is responsible for refunding `amount - pay` externally.
49+ //! Callers that pattern-matched `Ok(())` must update to accept `Ok(pay)`.
50+ //! - `top_up_insurance_fund` return type: `Result<bool>` → `Result<()>`.
51+ //! The returned `bool` (post-balance > 0) carried no caller-useful
52+ //! signal and was dropped in v12.19.
3253
3354#![ no_std]
3455#![ forbid( unsafe_code) ]
@@ -1248,6 +1269,28 @@ impl RiskEngine {
12481269 if self . accounts[ i] . fee_credits. get( ) != 0 {
12491270 return Err ( RiskError :: CorruptState ) ;
12501271 }
1272+ // Free-list head validation (reviewer pass finding #1). Before any
1273+ // mutation, prove that `free_head` is safe to prepend to:
1274+ // (a) head is u16::MAX (empty list) OR
1275+ // (b) head is in [0, MAX_ACCOUNTS) AND the slot is not used AND
1276+ // the slot's prev_free == u16::MAX (it is genuinely the head).
1277+ // A corrupt head that lands on a used slot would graft it into the
1278+ // free list; a corrupt head at a non-head free node would overwrite
1279+ // that node's prev_free pointer. Both are allocator-corruption paths
1280+ // that must fail conservatively rather than be silently stitched
1281+ // through.
1282+ if self . free_head != u16 :: MAX {
1283+ let h = self . free_head as usize ;
1284+ if h >= MAX_ACCOUNTS {
1285+ return Err ( RiskError :: CorruptState ) ;
1286+ }
1287+ if self . is_used( h) {
1288+ return Err ( RiskError :: CorruptState ) ;
1289+ }
1290+ if self . prev_free[ h] != u16 :: MAX {
1291+ return Err ( RiskError :: CorruptState ) ;
1292+ }
1293+ }
12511294 let a = & mut self . accounts[ i] ;
12521295 a. capital = U128 :: ZERO ;
12531296 a. kind = Account :: KIND_USER ;
@@ -1273,14 +1316,6 @@ impl RiskEngine {
12731316 a. pending_remaining_q = 0 ;
12741317 a. pending_horizon = 0 ;
12751318 a. pending_created_slot = 0 ;
1276- // Bounds-check free_head before indexing: a corrupt free_head
1277- // value in range [MAX_ACCOUNTS, u16::MAX) would panic at the
1278- // prev_free[...] write below, violating spec §0 goal 24's
1279- // deterministic-conservative-failure rule. Either u16::MAX (empty)
1280- // or a valid in-range index is acceptable.
1281- if self . free_head != u16 :: MAX && ( self . free_head as usize ) >= MAX_ACCOUNTS {
1282- return Err ( RiskError :: CorruptState ) ;
1283- }
12841319 self . clear_used( i) ;
12851320 // Push to head of doubly-linked free list.
12861321 self . next_free[ i] = self . free_head;
@@ -2837,13 +2872,17 @@ impl RiskEngine {
28372872 }
28382873 }
28392874
2840- // Step 8 (§5.6 step 8): if OI_post == 0
2875+ // Step 8 (§5.6 step 8): if OI_post == 0, BOTH flags MUST be set.
2876+ // The prior impl gated the liq_side flag on `self.get_oi_eff(liq_side)
2877+ // == 0`, which matched the spec only under valid bilateral symmetry
2878+ // (where OI_long == OI_short, so liq_side OI is also 0). Under
2879+ // corrupt-imbalance states the gating diverged from spec and left
2880+ // the liq_side flag unset — not fail-conservative. Per spec §5.6
2881+ // step 8 text, the flag is unconditional.
28412882 if oi_post == 0 {
28422883 self . set_oi_eff( opp, 0u128 ) ;
28432884 set_pending_reset( ctx, opp) ;
2844- if self . get_oi_eff( liq_side) == 0 {
2845- set_pending_reset( ctx, liq_side) ;
2846- }
2885+ set_pending_reset( ctx, liq_side) ;
28472886 return Ok ( ( ) ) ;
28482887 }
28492888
@@ -3439,6 +3478,31 @@ impl RiskEngine {
34393478 if self . stored_pos_count_long > cap || self . stored_pos_count_short > cap {
34403479 return Err ( RiskError :: CorruptState ) ;
34413480 }
3481+ // Cheap O(1) global invariants expanded in v12.19 per reviewer audit:
3482+ // Spec §2.2 / §3.2: pnl_matured_pos_tot <= pnl_pos_tot.
3483+ if self . pnl_matured_pos_tot > self . pnl_pos_tot {
3484+ return Err ( RiskError :: CorruptState ) ;
3485+ }
3486+ // Spec §1.4: materialized_account_count <= MAX_MATERIALIZED_ACCOUNTS.
3487+ if self . materialized_account_count > MAX_MATERIALIZED_ACCOUNTS {
3488+ return Err ( RiskError :: CorruptState ) ;
3489+ }
3490+ // Spec §4.7 v12.16.4: neg_pnl_account_count <= materialized_account_count.
3491+ if self . neg_pnl_account_count > self . materialized_account_count {
3492+ return Err ( RiskError :: CorruptState ) ;
3493+ }
3494+ // Spec §2.2 v12.19: rr_cursor_position < MAX_MATERIALIZED_ACCOUNTS.
3495+ if self . rr_cursor_position >= MAX_MATERIALIZED_ACCOUNTS {
3496+ return Err ( RiskError :: CorruptState ) ;
3497+ }
3498+ // Spec §6.8: when resolved payout snapshot is ready, h_num <= h_den.
3499+ // Before ready, both should be zero (checked by the ready = 0 branch
3500+ // in capture_resolved_payout_snapshot_if_needed callers).
3501+ if self . resolved_payout_ready != 0
3502+ && self . resolved_payout_h_num > self . resolved_payout_h_den
3503+ {
3504+ return Err ( RiskError :: CorruptState ) ;
3505+ }
34423506 Ok ( ( ) )
34433507 }
34443508
@@ -4073,9 +4137,10 @@ impl RiskEngine {
40734137 // Spec §12.21: public wrappers MUST NOT combine
40744138 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
40754139 // The engine accepts the combination because it cannot distinguish
4076- // trusted/private wrappers (for which it is permitted) from public
4077- // wrappers. Compliance is a wrapper-layer obligation; engine-level
4078- // invariants still hold per property 107.
4140+ // trusted/private wrappers (permitted) from public wrappers
4141+ // (forbidden) at this layer. Compliance is enforced above the
4142+ // engine. Engine-level invariants still hold per property 107
4143+ // (the v19_cascade_safety Kani proof).
40794144
40804145 if oracle_price == 0 || oracle_price > MAX_ORACLE_PRICE {
40814146 return Err ( RiskError :: Overflow ) ;
@@ -4201,9 +4266,10 @@ impl RiskEngine {
42014266 // Spec §12.21: public wrappers MUST NOT combine
42024267 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
42034268 // The engine accepts the combination because it cannot distinguish
4204- // trusted/private wrappers (for which it is permitted) from public
4205- // wrappers. Compliance is a wrapper-layer obligation; engine-level
4206- // invariants still hold per property 107.
4269+ // trusted/private wrappers (permitted) from public wrappers
4270+ // (forbidden) at this layer. Compliance is enforced above the
4271+ // engine. Engine-level invariants still hold per property 107
4272+ // (the v19_cascade_safety Kani proof).
42074273
42084274 if oracle_price == 0 || oracle_price > MAX_ORACLE_PRICE {
42094275 return Err ( RiskError :: Overflow ) ;
@@ -4286,9 +4352,10 @@ impl RiskEngine {
42864352 // Spec §12.21: public wrappers MUST NOT combine
42874353 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
42884354 // The engine accepts the combination because it cannot distinguish
4289- // trusted/private wrappers (for which it is permitted) from public
4290- // wrappers. Compliance is a wrapper-layer obligation; engine-level
4291- // invariants still hold per property 107.
4355+ // trusted/private wrappers (permitted) from public wrappers
4356+ // (forbidden) at this layer. Compliance is enforced above the
4357+ // engine. Engine-level invariants still hold per property 107
4358+ // (the v19_cascade_safety Kani proof).
42924359
42934360 if oracle_price == 0 || oracle_price > MAX_ORACLE_PRICE {
42944361 return Err ( RiskError :: Overflow ) ;
@@ -4811,9 +4878,10 @@ impl RiskEngine {
48114878 // Spec §12.21: public wrappers MUST NOT combine
48124879 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
48134880 // The engine accepts the combination because it cannot distinguish
4814- // trusted/private wrappers (for which it is permitted) from public
4815- // wrappers. Compliance is a wrapper-layer obligation; engine-level
4816- // invariants still hold per property 107.
4881+ // trusted/private wrappers (permitted) from public wrappers
4882+ // (forbidden) at this layer. Compliance is enforced above the
4883+ // engine. Engine-level invariants still hold per property 107
4884+ // (the v19_cascade_safety Kani proof).
48174885
48184886 // Spec §9.6 step 2: require account materialized (public entry point).
48194887 if ( idx as usize ) >= MAX_ACCOUNTS || !self . is_used ( idx as usize ) {
@@ -5049,9 +5117,10 @@ impl RiskEngine {
50495117 // Spec §12.21: public wrappers MUST NOT combine
50505118 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
50515119 // The engine accepts the combination because it cannot distinguish
5052- // trusted/private wrappers (for which it is permitted) from public
5053- // wrappers. Compliance is a wrapper-layer obligation; engine-level
5054- // invariants still hold per property 107.
5120+ // trusted/private wrappers (permitted) from public wrappers
5121+ // (forbidden) at this layer. Compliance is enforced above the
5122+ // engine. Engine-level invariants still hold per property 107
5123+ // (the v19_cascade_safety Kani proof).
50555124
50565125 if oracle_price == 0 || oracle_price > MAX_ORACLE_PRICE {
50575126 return Err ( RiskError :: Overflow ) ;
@@ -5318,9 +5387,10 @@ impl RiskEngine {
53185387 // Spec §12.21: public wrappers MUST NOT combine
53195388 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
53205389 // The engine accepts the combination because it cannot distinguish
5321- // trusted/private wrappers (for which it is permitted) from public
5322- // wrappers. Compliance is a wrapper-layer obligation; engine-level
5323- // invariants still hold per property 107.
5390+ // trusted/private wrappers (permitted) from public wrappers
5391+ // (forbidden) at this layer. Compliance is enforced above the
5392+ // engine. Engine-level invariants still hold per property 107
5393+ // (the v19_cascade_safety Kani proof).
53245394
53255395 if oracle_price == 0 || oracle_price > MAX_ORACLE_PRICE {
53265396 return Err ( RiskError :: Overflow ) ;
@@ -5440,9 +5510,10 @@ impl RiskEngine {
54405510 // Spec §12.21: public wrappers MUST NOT combine
54415511 // (admit_h_min == 0, admit_h_max_consumption_threshold_bps_opt = None).
54425512 // The engine accepts the combination because it cannot distinguish
5443- // trusted/private wrappers (for which it is permitted) from public
5444- // wrappers. Compliance is a wrapper-layer obligation; engine-level
5445- // invariants still hold per property 107.
5513+ // trusted/private wrappers (permitted) from public wrappers
5514+ // (forbidden) at this layer. Compliance is enforced above the
5515+ // engine. Engine-level invariants still hold per property 107
5516+ // (the v19_cascade_safety Kani proof).
54465517
54475518 if self . market_mode != MarketMode :: Live {
54485519 return Err ( RiskError :: Unauthorized ) ;
0 commit comments