fix: v11.26 spec compliance — flat-close guard, fee-neutral risk-reducing, constants

v11.26 change aeyakovenko#2 — Flat-close guard uses Eq_maint_raw_i >= 0:
  enforce_one_side_margin now checks account_equity_maint_raw_wide >= 0
  for flat exits, not just pnl >= 0. Prevents flat exit with negative
  net wealth from fee debt (C + PNL - FeeDebt < 0).
  TDD: proof_v1126_flat_close_uses_eq_maint_raw (19s, PASS)

v11.26 change #1 — Fee-neutral risk-reducing exemption:
  Buffer comparison now adds fee back: (Eq_maint_raw_post + fee) - MM_req_post.
  Also enforces shortfall guard: min(Eq_maint_raw_post + fee, 0) >= min(pre, 0).
  Pure fee friction no longer blocks genuine de-risking trades.
  TDD: proof_v1126_risk_reducing_fee_neutral (18s, 1/1 cover)

Other fixes:
  - MAX_TRADE_SIZE_Q: 200T → MAX_POSITION_ABS_Q (100T) per spec §1.4
  - liquidate_at_oracle OI assertion now unconditional per spec §10.6 step 10
  - enforce_one_side_margin takes fee parameter for fee-neutral comparison

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: aeyakovenko

src/percolator.rs

@@ -58,7 +58,7 @@ pub const MAX_ABS_FUNDING_BPS_PER_SLOT: i64 = 10_000;
 pub const MAX_VAULT_TVL: u128 = 10_000_000_000_000_000;
 pub const MAX_POSITION_ABS_Q: u128 = 100_000_000_000_000;
 pub const MAX_ACCOUNT_NOTIONAL: u128 = 100_000_000_000_000_000_000;
-pub const MAX_TRADE_SIZE_Q: u128 = 200_000_000_000_000;
+pub const MAX_TRADE_SIZE_Q: u128 = MAX_POSITION_ABS_Q; // spec §1.4
 pub const MAX_OI_SIDE_Q: u128 = 100_000_000_000_000;
 pub const MAX_MATERIALIZED_ACCOUNTS: u64 = 1_000_000;
 pub const MAX_ACCOUNT_POSITIVE_PNL: u128 = 100_000_000_000_000_000_000_000_000_000_000;
@@ -2402,7 +2402,7 @@ impl RiskEngine {
         self.enforce_post_trade_margin(
             a as usize, b as usize, oracle_price,
             &old_eff_a, &new_eff_a, &old_eff_b, &new_eff_b,
-            buffer_pre_a, buffer_pre_b,
+            buffer_pre_a, buffer_pre_b, fee,
         )?;
 
         // Steps 16-17: end-of-instruction resets
@@ -2486,9 +2486,10 @@ impl RiskEngine {
         new_eff_b: &i128,
         buffer_pre_a: I256,
         buffer_pre_b: I256,
+        fee: u128,
     ) -> Result<()> {
-        self.enforce_one_side_margin(a, oracle_price, old_eff_a, new_eff_a, buffer_pre_a)?;
-        self.enforce_one_side_margin(b, oracle_price, old_eff_b, new_eff_b, buffer_pre_b)?;
+        self.enforce_one_side_margin(a, oracle_price, old_eff_a, new_eff_a, buffer_pre_a, fee)?;
+        self.enforce_one_side_margin(b, oracle_price, old_eff_b, new_eff_b, buffer_pre_b, fee)?;
         Ok(())
     }
 
@@ -2499,10 +2500,13 @@ impl RiskEngine {
         old_eff: &i128,
         new_eff: &i128,
         buffer_pre: I256,
+        fee: u128,
     ) -> Result<()> {
         if *new_eff == 0 {
-            // Flat: PnL must be >= 0 after settle_losses (steps 25-26)
-            if self.accounts[idx].pnl < 0 {
+            // v11.26 §10.5 step 29: flat-close guard uses exact Eq_maint_raw_i >= 0
+            // (not just PNL >= 0). Prevents flat exits with negative net wealth from fee debt.
+            let maint_raw = self.account_equity_maint_raw_wide(&self.accounts[idx]);
+            if maint_raw.is_negative() {
                 return Err(RiskError::Undercollateralized);
             }
             return Ok(());
@@ -2531,32 +2535,42 @@ impl RiskEngine {
         } else if self.is_above_maintenance_margin(&self.accounts[idx], idx, oracle_price) {
             // Maintenance healthy: allow
         } else if strictly_reducing {
-            // Strict risk-reducing: allow only if post-trade raw maintenance buffer
-            // is strictly greater than pre-trade buffer (spec §10.5 step 29)
-            // Uses exact I256 per §3.4 — no saturation or clamping.
-            //
-            // Additionally, raw equity must not decrease (accounting for fees):
-            // Eq_maint_raw_post + fee >= Eq_maint_raw_pre
-            // This prevents execution slippage from being weaponized to siphon
-            // money from a bankrupt account (buffer masking via MM_req drop).
+            // v11.26 §10.5 step 29: strict risk-reducing exemption (fee-neutral).
+            // Both conditions must hold in exact widened I256:
+            // 1. Fee-neutral buffer improves: (Eq_maint_raw_post + fee) - MM_req_post > buffer_pre
+            // 2. Fee-neutral shortfall does not worsen: min(Eq_maint_raw_post + fee, 0) >= min(Eq_maint_raw_pre, 0)
             let maint_raw_wide_post = self.account_equity_maint_raw_wide(&self.accounts[idx]);
-            let maint_raw_wide_pre = buffer_pre.checked_add(I256::from_u128({
+            let fee_wide = I256::from_u128(fee);
+
+            // Fee-neutral post equity and buffer
+            let maint_raw_fee_neutral = maint_raw_wide_post.checked_add(fee_wide).expect("I256 add");
+            let mm_req_post = {
+                let not = self.notional(idx, oracle_price);
+                mul_u128(not, self.params.maintenance_margin_bps as u128) / 10_000
+            };
+            let buffer_post_fee_neutral = maint_raw_fee_neutral.checked_sub(I256::from_u128(mm_req_post)).expect("I256 sub");
+
+            // Recover pre-trade raw equity from buffer_pre + MM_req_pre
+            let mm_req_pre = {
                 let not_pre = if *old_eff == 0 { 0u128 } else {
                     mul_div_floor_u128(old_eff.unsigned_abs(), oracle_price as u128, POS_SCALE)
                 };
                 mul_u128(not_pre, self.params.maintenance_margin_bps as u128) / 10_000
-            })).expect("I256 add");
-            // Guard: raw equity must not decrease (prevents slippage extraction)
-            if maint_raw_wide_post < maint_raw_wide_pre {
-                return Err(RiskError::Undercollateralized);
-            }
-            let mm_req_post = {
-                let not = self.notional(idx, oracle_price);
-                mul_u128(not, self.params.maintenance_margin_bps as u128) / 10_000
             };
-            let buffer_post = maint_raw_wide_post.checked_sub(I256::from_u128(mm_req_post)).expect("I256 sub");
-            if buffer_post > buffer_pre {
-                // Improved: allow
+            let maint_raw_pre = buffer_pre.checked_add(I256::from_u128(mm_req_pre)).expect("I256 add");
+
+            // Condition 1: fee-neutral buffer strictly improves
+            let cond1 = buffer_post_fee_neutral > buffer_pre;
+
+            // Condition 2: fee-neutral shortfall below zero does not worsen
+            // min(post + fee, 0) >= min(pre, 0)
+            let zero = I256::from_i128(0);
+            let shortfall_post = if maint_raw_fee_neutral < zero { maint_raw_fee_neutral } else { zero };
+            let shortfall_pre = if maint_raw_pre < zero { maint_raw_pre } else { zero };
+            let cond2 = shortfall_post >= shortfall_pre;
+
+            if cond1 && cond2 {
+                // Both conditions met: allow
             } else {
                 return Err(RiskError::Undercollateralized);
             }
@@ -2630,10 +2644,9 @@ impl RiskEngine {
         self.finalize_end_of_instruction_resets(&ctx);
         self.recompute_r_last_from_final_state();
 
-        if result {
-            // Assert OI balance (spec §10.5)
-            assert!(self.oi_eff_long_q == self.oi_eff_short_q, "OI_eff_long != OI_eff_short after liquidation");
-        }
+        // Assert OI balance unconditionally (spec §10.6 step 10)
+        // touch_account_full mutates side state even when liquidation doesn't proceed.
+        assert!(self.oi_eff_long_q == self.oi_eff_short_q, "OI_eff_long != OI_eff_short after liquidation");
         Ok(result)
     }
 

tests/proofs_safety.rs

@@ -1170,3 +1170,127 @@ fn proof_settle_fee_rejects_i128_min() {
     assert!(result.is_err(),
         "engine must reject fee decrement that would produce i128::MIN");
 }
+
+// ############################################################################
+// v11.26 compliance: flat-close guard uses Eq_maint_raw_i >= 0
+// ############################################################################
+
+/// v11.26 change #2: A trade that closes to flat must use Eq_maint_raw_i >= 0,
+/// not just PNL_i >= 0. An account with positive PNL but large fee debt
+/// (Eq_maint_raw_i = C + PNL - FeeDebt < 0) must be rejected.
+#[kani::proof]
+#[kani::unwind(70)]
+#[kani::solver(cadical)]
+fn proof_v1126_flat_close_uses_eq_maint_raw() {
+    let mut params = zero_fee_params();
+    params.trading_fee_bps = 100; // 1% fee
+    let mut engine = RiskEngine::new(params);
+    engine.last_crank_slot = DEFAULT_SLOT;
+
+    let a = engine.add_user(0).unwrap();
+    let b = engine.add_user(0).unwrap();
+    engine.deposit(a, 100_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap();
+    engine.deposit(b, 500_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap();
+
+    // Open position for a
+    let size = (500 * POS_SCALE) as i128;
+    engine.execute_trade(a, b, DEFAULT_ORACLE, DEFAULT_SLOT, size, DEFAULT_ORACLE).unwrap();
+
+    // Drain a's capital to 0, give positive PNL but massive fee debt
+    engine.set_capital(a as usize, 0);
+    engine.set_pnl(a as usize, 1000i128); // positive PNL
+    engine.accounts[a as usize].fee_credits = I128::new(-5000); // fee debt
+
+    // Eq_maint_raw = C(0) + PNL(1000) - FeeDebt(5000) = -4000 < 0
+    // v11.26 requires: reject flat close when Eq_maint_raw < 0
+    // Old code only checks PNL >= 0 which would pass (PNL = 1000 > 0)
+
+    let close_size = -size;
+    let result = engine.execute_trade(a, b, DEFAULT_ORACLE, DEFAULT_SLOT, close_size, DEFAULT_ORACLE);
+
+    // Must be rejected: Eq_maint_raw < 0 even though PNL > 0
+    assert!(result.is_err(),
+        "v11.26: flat close must be rejected when Eq_maint_raw < 0 (fee debt exceeds C + PNL)");
+}
+
+// ############################################################################
+// v11.26 compliance: risk-reducing exemption is fee-neutral
+// ############################################################################
+
+/// v11.26 change #1: The risk-reducing buffer comparison must be fee-neutral.
+/// A genuine de-risking trade must not fail solely because the trading fee
+/// reduces post-trade equity.
+#[kani::proof]
+#[kani::unwind(70)]
+#[kani::solver(cadical)]
+fn proof_v1126_risk_reducing_fee_neutral() {
+    let mut params = zero_fee_params();
+    params.trading_fee_bps = 100; // 1% fee to make fee friction visible
+    let mut engine = RiskEngine::new(params);
+    engine.last_crank_slot = DEFAULT_SLOT;
+
+    let a = engine.add_user(0).unwrap();
+    let b = engine.add_user(0).unwrap();
+    engine.deposit(a, 100_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap();
+    engine.deposit(b, 500_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap();
+
+    // Open leveraged position
+    let size = (800 * POS_SCALE) as i128;
+    engine.execute_trade(a, b, DEFAULT_ORACLE, DEFAULT_SLOT, size, DEFAULT_ORACLE).unwrap();
+
+    // Push below maintenance
+    engine.set_pnl(a as usize, -50_000i128);
+
+    // Risk-reducing: close half at oracle price (no slippage)
+    let half_close = -(size / 2);
+    let result = engine.execute_trade(a, b, DEFAULT_ORACLE, DEFAULT_SLOT, half_close, DEFAULT_ORACLE);
+
+    // v11.26: fee-neutral comparison means pure fee friction should not block
+    // a genuine de-risking trade at oracle price.
+    // The post-trade buffer (with fee added back) should be strictly better.
+    // Conservation must hold regardless of whether trade succeeds or fails.
+    assert!(engine.check_conservation());
+    kani::cover!(result.is_ok(), "fee-neutral risk-reducing trade accepted");
+}
+
+// ############################################################################
+// v11.26 compliance: MIN_NONZERO_MM_REQ floor (TODO: implement params first)
+// ############################################################################
+
+// Commented out until RiskParams gains min_nonzero_mm_req / min_nonzero_im_req
+/*
+#[kani::proof]
+#[kani::unwind(70)]
+#[kani::solver(cadical)]
+fn proof_v1126_min_nonzero_margin_floor() {
+    let mut params = zero_fee_params();
+    params.min_nonzero_mm_req = 1000;   // $0.001 floor
+    params.min_nonzero_im_req = 2000;   // $0.002 floor
+    let mut engine = RiskEngine::new(params);
+    engine.last_crank_slot = DEFAULT_SLOT;
+
+    let a = engine.add_user(0).unwrap();
+    let b = engine.add_user(0).unwrap();
+    engine.deposit(a, 100_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap();
+    engine.deposit(b, 500_000, DEFAULT_ORACLE, DEFAULT_SLOT).unwrap();
+
+    // Tiny position: notional so small that proportional MM floors to 0
+    let tiny_size = 1i128; // 1 unit of position
+    let result = engine.execute_trade(a, b, DEFAULT_ORACLE, DEFAULT_SLOT, tiny_size, DEFAULT_ORACLE);
+
+    if result.is_ok() {
+        // The position exists with nonzero effective pos
+        let eff = engine.effective_pos_q(a as usize);
+        if eff != 0 {
+            // MM_req must be at least MIN_NONZERO_MM_REQ
+            let notional = engine.notional(a as usize, DEFAULT_ORACLE);
+            let proportional_mm = mul_u128(notional, params.maintenance_margin_bps as u128) / 10_000;
+            // If proportional floors to 0, the min floor must apply
+            if proportional_mm == 0 {
+                kani::cover!(true, "proportional MM floors to 0 — min floor must apply");
+            }
+        }
+    }
+    assert!(engine.check_conservation());
+}
+*/