diff --git a/src/math.rs b/src/math.rs
index a7e9db3..201ada7 100644
--- a/src/math.rs
+++ b/src/math.rs
@@ -124,6 +124,38 @@ pub fn calc_junior_lp_for_deposit(
     calc_lp_for_deposit(junior_total_lp, junior_balance, deposit_amount)
 }
 
+/// Calculate LP tokens for a senior tranche deposit.
+///
+/// The senior tranche has its own sub-pool: `senior_balance / senior_total_lp`,
+/// where `senior_balance = total_pool_value - effective_junior_balance` and
+/// `senior_total_lp = total_lp_supply - junior_total_lp`.
+///
+/// This MUST price against the same basis the senior WITHDRAW path values against
+/// (`calc_senior_collateral_for_withdraw`), so a senior deposit-then-withdraw
+/// round-trip cannot profit. Pricing senior deposits at the GLOBAL ratio while
+/// redeeming at the senior ratio lets a depositor mint cheap and redeem dear after
+/// a junior-absorbed loss, extracting value from existing senior LPs. Delegates to
+/// `calc_lp_for_deposit`, inheriting its round-DOWN (pool-favoring) semantics AND
+/// its first-depositor / orphaned-value (C9) handling: a true first senior deposit
+/// (`senior_total_lp == 0 && senior_balance == 0` — empty pool, or junior-first
+/// where junior captures 100% of fees) mints 1:1, while ORPHANED senior value
+/// (`senior_total_lp == 0 && senior_balance > 0`, e.g. insurance returned after all
+/// senior LP exited) returns `None` so the caller REJECTS the deposit. Minting 1:1
+/// against an orphan would let a dust deposit redeem the whole orphaned balance, so
+/// the caller MUST NOT special-case `senior_total_lp == 0` into an unconditional
+/// 1:1 bootstrap — it defers to this guard, exactly as the non-tranche path does.
+///
+/// # Returns
+/// * `Some(lp_tokens)` to mint (rounds DOWN — pool-favoring, same as junior/global)
+/// * `None` on overflow or blocked state (orphaned value)
+pub fn calc_senior_lp_for_deposit(
+    senior_total_lp: u64,
+    senior_balance: u64,
+    deposit_amount: u64,
+) -> Option<u64> {
+    calc_lp_for_deposit(senior_total_lp, senior_balance, deposit_amount)
+}
+
 /// Calculate collateral for a junior LP token burn.
 ///
 /// Junior withdrawals are valued against the junior sub-pool only.
@@ -261,12 +293,12 @@ pub fn distribute_fees(
         let q = (total_fee as u128) / total_weight;
         let r = (total_fee as u128) % total_weight;
         let part1 = q * junior_weight; // q ≤ 2^64, junior_weight ≤ 2^80 → fits u128
-        // For part2: r < total_weight ≤ 2^81, junior_weight ≤ 2^80 → product ≤ 2^161
-        // Use checked_mul; if it overflows clamp part2 to total_fee (conservative safe bound).
-        let part2 = r
-            .checked_mul(junior_weight)
-            .map(|p| p / total_weight)
-            .unwrap_or(total_fee as u128);
+        // part2 = floor(r * junior_weight / total_weight). r < total_weight ≤ ~2^81 and
+        // junior_weight ≤ ~2^80, so r * junior_weight (~2^161) overflows u128. The previous
+        // `unwrap_or(total_fee)` fallback on that overflow handed junior 100% of the fee
+        // (0% to the protected senior tranche) — see #120. Use an exact, overflow-safe
+        // 256-bit mul-div instead. The true result is < junior_weight ≤ ~2^80, so it fits.
+        let part2 = mul_div_floor(r, junior_weight, total_weight);
         part1.saturating_add(part2)
     };
     // Clamp to total_fee (should always hold since junior_weight <= total_weight)
@@ -276,6 +308,54 @@ pub fn distribute_fees(
     (junior_fee, senior_fee)
 }
 
+/// Exact `floor(a * b / d)` for u128 operands, overflow-safe even when `a * b`
+/// exceeds u128. Requires `d != 0` and the true quotient to fit in u128 (callers
+/// guarantee this: here `b <= d`, so the quotient is `<= a`). Used by
+/// `distribute_fees` so the fee split is correct at extreme balances/fee values
+/// where the naive `a * b` overflows (#120).
+fn mul_div_floor(a: u128, b: u128, d: u128) -> u128 {
+    // Fast path: the product fits in u128.
+    if let Some(p) = a.checked_mul(b) {
+        return p / d;
+    }
+    // Slow path: form the full 256-bit product a*b = hi*2^128 + lo via 64-bit limbs,
+    // then long-divide (hi:lo) by d bit by bit.
+    let mask = u64::MAX as u128;
+    let (a0, a1) = (a & mask, a >> 64);
+    let (b0, b1) = (b & mask, b >> 64);
+    let m0 = a0 * b0; // each < 2^128
+    let m1 = a0 * b1;
+    let m2 = a1 * b0;
+    let m3 = a1 * b1;
+    // mid = m1 + m2 (the cross terms), tracking the carry bit that overflows u128.
+    let (mid, mid_carry) = {
+        let (s, c) = m1.overflowing_add(m2);
+        (s, c as u128)
+    };
+    // lo = m0 + (mid_low << 64); carry + mid_high + mid_carry + m3 go to hi.
+    let (lo, c1) = m0.overflowing_add(mid << 64);
+    let hi = m3 + (mid >> 64) + (mid_carry << 64) + (c1 as u128);
+    // Long division of (hi:lo) by d. The quotient fits u128 because the true result
+    // is <= a; bits at positions >= 128 are therefore always 0.
+    let mut rem: u128 = 0;
+    let mut quo: u128 = 0;
+    let mut i: u32 = 256;
+    while i > 0 {
+        i -= 1;
+        let bit = if i >= 128 { (hi >> (i - 128)) & 1 } else { (lo >> i) & 1 };
+        let rem_top = rem >> 127; // bit shifted out of the 128-bit rem below
+        rem = (rem << 1) | bit;
+        // Compare the true remainder (rem_top:rem) against d; reduce if >=.
+        if rem_top == 1 || rem >= d {
+            rem = rem.wrapping_sub(d);
+            if i < 128 {
+                quo |= 1u128 << i;
+            }
+        }
+    }
+    quo
+}
+
 /// Check senior never loses while junior is positive.
 ///
 /// Given initial senior balance and post-loss senior balance,
@@ -614,6 +694,36 @@ mod tests {
         assert_eq!(calc_junior_lp_for_deposit(1000, 2000, 500), Some(250));
     }
 
+    #[test]
+    fn test_senior_first_deposit_1_to_1() {
+        // True first senior depositor (empty senior sub-pool) → 1:1.
+        assert_eq!(calc_senior_lp_for_deposit(0, 0, 1000), Some(1000));
+    }
+
+    #[test]
+    fn test_senior_pro_rata() {
+        // Senior sub-pool worth 2x → half the LP per token (rounds down, pool-favoring).
+        assert_eq!(calc_senior_lp_for_deposit(1000, 2000, 500), Some(250));
+    }
+
+    #[test]
+    fn test_senior_deposit_orphaned_value_blocked() {
+        // Senior LP supply 0 but senior balance > 0 (orphaned value): the math
+        // helper blocks (the caller `process_deposit` handles the legitimate
+        // first-senior bootstrap via its `senior_total_lp() == 0` branch).
+        assert_eq!(calc_senior_lp_for_deposit(0, 500, 1000), None);
+    }
+
+    #[test]
+    fn test_senior_deposit_round_trip_no_profit_after_loss() {
+        // Deposit then immediate withdraw on the senior sub-pool must not profit.
+        // Senior sub-pool after a junior-absorbed loss: senior_total_lp=1000, senior_balance=1000.
+        let lp = calc_senior_lp_for_deposit(1000, 1000, 1000).unwrap(); // 1000 LP
+        // After deposit, senior_total_lp=2000, senior_balance=2000.
+        let back = calc_senior_collateral_for_withdraw(2000, 2000, lp).unwrap();
+        assert!(back <= 1000, "senior round-trip must not profit (got {back})");
+    }
+
     #[test]
     fn test_junior_withdraw_proportional() {
         assert_eq!(
@@ -694,6 +804,53 @@ mod tests {
         assert_eq!(sf, 0);
     }
 
+    // #120: at extreme balances/fee the inner `r * junior_weight` overflows u128.
+    // The old fallback handed junior 100%; these assert the exact proportional split.
+    // Expected values computed with arbitrary-precision integers (junior = floor(
+    // total_fee * junior_weight / total_weight), senior = total_fee - junior).
+    #[test]
+    fn test_distribute_fees_overflow_proportional() {
+        let max = u64::MAX;
+        // Symmetric, 5x junior mult → junior weight 50000, senior 10000 → 5/6 vs 1/6.
+        let (jf, sf) = distribute_fees(max, max, 50000, max);
+        assert_eq!(jf, 15372286728091293012);
+        assert_eq!(sf, 3074457345618258603);
+        assert_eq!((jf as u128) + (sf as u128), max as u128); // conservation
+        assert!(sf > 0, "#120: protected senior must not be zeroed out");
+
+        // Junior-heavy.
+        let (jf, sf) = distribute_fees(max, 1_000_000, 50000, max);
+        assert_eq!(jf, 18446744073709351615);
+        assert_eq!(sf, 200000);
+
+        // Senior-heavy.
+        let (jf, sf) = distribute_fees(1_000_000, max, 50000, max);
+        assert_eq!(jf, 4999999);
+        assert_eq!(sf, 18446744073704551616);
+
+        // Mid-range values that still overflow the naive product.
+        let (jf, sf) = distribute_fees(max / 2, max / 3, 30000, max / 7);
+        assert_eq!(jf, 2156112943680337201);
+        assert_eq!(sf, 479136209706741601);
+    }
+
+    #[test]
+    fn test_mul_div_floor_matches_native_when_product_fits() {
+        // Fast-path agreement with the native computation across a range of values.
+        for &(a, b, d) in &[
+            (1_000_000u128, 500_000u128, 1_500_000u128),
+            (0, 123, 7),
+            (u64::MAX as u128, 3, 7),
+            (12345678, 87654321, 999983),
+            (1, 1, 1),
+        ] {
+            assert_eq!(mul_div_floor(a, b, d), (a * b) / d);
+        }
+        // Slow-path (a*b overflows u128) sanity: floor(2^120 * 2^120 / 2^120) == 2^120.
+        let big = 1u128 << 120;
+        assert_eq!(mul_div_floor(big, big, big), big);
+    }
+
     #[test]
     fn test_senior_protected_when_junior_covers() {
         assert!(senior_protected(1000, 5000, 800));
diff --git a/src/processor.rs b/src/processor.rs
index 415a232..70a9ddc 100644
--- a/src/processor.rs
+++ b/src/processor.rs
@@ -22,12 +22,23 @@ fn verify_token_program(token_program: &AccountInfo) -> ProgramResult {
     Ok(())
 }
 
-/// Validate cooldown_slots parameter: must be > 0 to enforce cooldown.
+/// Upper bound on cooldown_slots (~1 year at ~2.5 slots/sec ≈ 78.84M slots). Long
+/// enough for any realistic withdrawal cooldown, but finite so an admin cannot set
+/// cooldown_slots = u64::MAX (via InitPool/UpdateConfig) and permanently lock
+/// withdrawals — `clock.slot` would never reach the saturating deadline (#121).
+const MAX_COOLDOWN_SLOTS: u64 = 78_840_000;
+
+/// Validate cooldown_slots parameter: must be > 0 to enforce cooldown, and bounded
+/// above so it cannot be used to permanently freeze withdrawals.
 fn validate_cooldown_slots(cooldown_slots: u64) -> ProgramResult {
     if cooldown_slots == 0 {
         msg!("Invalid cooldown_slots: cannot be 0 (would disable cooldown protection)");
         return Err(ProgramError::InvalidArgument);
     }
+    if cooldown_slots > MAX_COOLDOWN_SLOTS {
+        msg!("Invalid cooldown_slots: exceeds maximum (~1 year of slots); would permanently lock withdrawals");
+        return Err(ProgramError::InvalidArgument);
+    }
     Ok(())
 }
 
@@ -454,10 +465,53 @@ fn process_deposit(program_id: &Pubkey, accounts: &[AccountInfo], amount: u64) -
         }
     }
 
-    // Calculate LP tokens to mint
-    let lp_to_mint = pool
-        .calc_lp_for_deposit(amount)
-        .ok_or(StakeError::Overflow)?;
+    // #136: crystallize any pending trading-fee surplus into share price BEFORE pricing
+    // this deposit, so LP cannot be minted at the stale pre-accrual price and capture
+    // fees earned before the depositor joined. Mode-1 only; read the vault balance here
+    // (before the user->vault transfer below) so only the fee surplus — not this deposit's
+    // own collateral — is folded. pool.vault == vault.key was verified above.
+    if pool.pool_mode == 1 {
+        if *vault.owner != crate::spl_token::id() {
+            return Err(ProgramError::IllegalOwner);
+        }
+        let current_balance = {
+            let vault_data = vault.try_borrow_data()?;
+            crate::spl_token::state::Account::unpack(&vault_data)?.amount
+        };
+        accrue_fees_inner(pool, current_balance)?;
+    }
+
+    // Calculate LP tokens to mint.
+    //
+    // When tranches are enabled this is the SENIOR deposit path (junior deposits
+    // go through process_deposit_junior). It MUST price against the senior
+    // sub-pool (senior_balance / senior_total_lp) — the same basis the senior
+    // WITHDRAW path values against (see calc_senior_collateral_for_withdraw) and
+    // mirroring process_deposit_junior. Pricing senior deposits at the GLOBAL
+    // ratio while redeeming at the senior ratio let an unprivileged user mint
+    // cheap and redeem dear after a junior-absorbed loss, extracting value from
+    // existing senior LPs.
+    //
+    // First-senior bootstrap and the orphaned-value (C9) guard are handled INSIDE
+    // calc_senior_lp_for_deposit (it delegates to calc_lp_for_deposit) — NOT
+    // special-cased here. A *true* first senior deposit has senior_balance == 0
+    // (an empty pool, or a junior-first pool where junior captures 100% of fees,
+    // so senior_balance stays 0), which mints 1:1. The ONLY state with
+    // senior_total_lp == 0 while senior_balance > 0 is ORPHANED senior value (all
+    // senior LP exited, then insurance was returned post-resolution): there the
+    // C9 guard returns None and we REJECT, exactly as the non-tranche path does.
+    // Seeding 1:1 against an orphan (an earlier version of this branch did) is a
+    // C9 bypass — a 1-token deposit would mint 1 LP against the orphan and redeem
+    // the whole orphaned balance. So senior_total_lp == 0 is NOT bootstrapped 1:1
+    // unconditionally; it defers to the same guard the global path uses.
+    let lp_to_mint = if pool.tranche_enabled() {
+        let senior_lp = pool.senior_total_lp();
+        let senior_bal = pool.senior_balance().ok_or(StakeError::Overflow)?;
+        crate::math::calc_senior_lp_for_deposit(senior_lp, senior_bal, amount)
+            .ok_or(StakeError::Overflow)?
+    } else {
+        pool.calc_lp_for_deposit(amount).ok_or(StakeError::Overflow)?
+    };
     // S-4: reject a zero-share mint EXPLICITLY (dedicated variant, not the generic
     // ZeroAmount). A nonzero deposit that rounds to 0 LP at the current share price
     // must never transfer collateral in while minting nothing. Share price derives
@@ -755,6 +809,22 @@ fn process_withdraw(
         is_junior = deposit._reserved[8] == 1;
     }
 
+    // #136: crystallize any pending trading-fee surplus into share price BEFORE pricing
+    // this withdrawal, so the withdrawer realizes their fair share of earned fees (and the
+    // HWM floor sees true TVL) rather than redeeming at the stale pre-accrual price.
+    // Mode-1 only; pool.vault == vault.key was verified above; read the balance before the
+    // vault->user transfer below.
+    if pool.pool_mode == 1 {
+        if *vault.owner != crate::spl_token::id() {
+            return Err(ProgramError::IllegalOwner);
+        }
+        let current_balance = {
+            let vault_data = vault.try_borrow_data()?;
+            crate::spl_token::state::Account::unpack(&vault_data)?.amount
+        };
+        accrue_fees_inner(pool, current_balance)?;
+    }
+
     // PERC-303: Determine withdrawal amount based on tranche
     let withdrawal_amount = if pool.tranche_enabled() && is_junior {
         // Junior withdrawal: valued against junior sub-pool after loss absorption.
@@ -1623,6 +1693,73 @@ fn process_rotate_insurance_authority(
 // PERC-272: LP Vault — Fee Accrual & Trading Pool Init
 // ============================================================================
 
+/// Crystallize any un-accrued vault surplus into pool share price. Shared by the
+/// permissionless `AccrueFees` instruction AND the deposit/withdraw pre-accrue guard
+/// (#136) so every pricing path applies byte-identical accounting.
+///
+/// `current_balance` MUST be the verified vault token-account balance read BEFORE any
+/// deposit transfer in the calling instruction — otherwise the deposit's own collateral
+/// would be mis-credited as fees. The caller must have already confirmed the vault key +
+/// SPL-Token ownership. Mutates only `pool`. No-op when there is no surplus or no LP
+/// holders, preserving the first-depositor bootstrap / anti-brick guard.
+fn accrue_fees_inner(pool: &mut state::StakePool, current_balance: u64) -> ProgramResult {
+    // total_pool_value() = deposited - withdrawn - flushed + returned + fees_earned (mode 1)
+    // — the authoritative expected balance; any excess is un-accrued fee revenue.
+    let pool_value = pool.total_pool_value().ok_or(StakeError::Overflow)?;
+
+    // Only accrue when there are active LP holders. Accruing at total_lp_supply == 0
+    // would set total_fees_earned > 0 at zero supply, tripping calc_lp_for_deposit's
+    // orphaned-value guard and permanently bricking the first deposit (an attacker can
+    // donate 1 token to the vault pre-first-deposit to trigger it).
+    if current_balance > pool_value && pool.total_lp_supply > 0 {
+        let fee_delta = current_balance - pool_value;
+
+        // Snapshot pre-fee tranche balances BEFORE incrementing total_fees_earned.
+        // senior_balance() derives from total_pool_value() which includes
+        // total_fees_earned, so reading it post-increment would inflate the senior
+        // weight in distribute_fees and systematically shortchange the junior tranche.
+        let distribute_to_junior = pool.tranche_enabled() && pool.junior_total_lp() > 0;
+        let (snapshot_junior_bal, snapshot_senior_bal) = if distribute_to_junior {
+            (
+                pool.junior_balance(),
+                pool.senior_balance().ok_or(StakeError::Overflow)?,
+            )
+        } else {
+            (0, 0)
+        };
+
+        pool.total_fees_earned = pool
+            .total_fees_earned
+            .checked_add(fee_delta)
+            .ok_or(StakeError::Overflow)?;
+
+        // PERC-303: distribute the fee delta between junior/senior sub-pools using the
+        // junior fee multiplier. Senior implicitly receives the remainder since
+        // senior_balance = total_pool_value() - junior_balance and total_fees_earned
+        // was already incremented by the full fee_delta above.
+        if distribute_to_junior {
+            let (junior_fee, _) = crate::math::distribute_fees(
+                snapshot_junior_bal,
+                snapshot_senior_bal,
+                pool.junior_fee_mult_bps(),
+                fee_delta,
+            );
+            pool.set_junior_balance(
+                pool.junior_balance()
+                    .checked_add(junior_fee)
+                    .ok_or(StakeError::Overflow)?,
+            );
+        }
+
+        msg!(
+            "AccrueFees: accrued {} fees, total_fees_earned={}",
+            fee_delta,
+            pool.total_fees_earned
+        );
+    }
+    Ok(())
+}
+
 /// Accrue trading fees from the percolator engine to the LP vault.
 /// Permissionless: reads vault token account balance and updates pool state.
 ///
@@ -1709,66 +1846,10 @@ fn process_accrue_fees(program_id: &Pubkey, accounts: &[AccountInfo]) -> Program
     // fee_delta, potentially double-counting or missing fees.
     // total_pool_value() = deposited - withdrawn - flushed + returned + fees_earned (mode 1)
     // which is the authoritative expected balance.
-    let pool_value = pool.total_pool_value().ok_or(StakeError::Overflow)?;
-
-    // Only accrue fees when there are active LP holders.
-    // If total_lp_supply == 0 and a balance surplus exists, accruing it would set
-    // total_fees_earned > 0 while total_lp_supply == 0.  The first depositor check in
-    // calc_lp_for_deposit (total_lp_supply==0 && pool_value==0) would then fail, blocking
-    // ALL future deposits and permanently locking the pool.  An attacker can trigger this
-    // by sending even 1 token directly to the vault before the first deposit.
-    if current_balance > pool_value && pool.total_lp_supply > 0 {
-        let fee_delta = current_balance - pool_value;
-
-        // Snapshot pre-fee tranche balances BEFORE incrementing total_fees_earned.
-        // senior_balance() derives from total_pool_value() which includes
-        // total_fees_earned.  Reading it after the increment inflates the senior
-        // weight in distribute_fees, systematically shortchanging the junior
-        // tranche (~6% per cycle on equal balances with a 2x multiplier).
-        let distribute_to_junior = pool.tranche_enabled() && pool.junior_total_lp() > 0;
-        let (snapshot_junior_bal, snapshot_senior_bal) = if distribute_to_junior {
-            (
-                pool.junior_balance(),
-                pool.senior_balance().ok_or(StakeError::Overflow)?,
-            )
-        } else {
-            (0, 0)
-        };
-
-        pool.total_fees_earned = pool
-            .total_fees_earned
-            .checked_add(fee_delta)
-            .ok_or(StakeError::Overflow)?;
-
-        // PERC-303: If tranches are active, distribute the fee delta between
-        // junior and senior sub-pools using the junior fee multiplier.
-        // Without this call, junior LPs receive ZERO benefit from junior_fee_mult_bps
-        // — all fees accrue to the global pool and senior LPs capture the entire yield.
-        // distribute_fees returns (junior_fee, senior_fee) that sum to <= fee_delta.
-        if distribute_to_junior {
-            let (junior_fee, _) = crate::math::distribute_fees(
-                snapshot_junior_bal,
-                snapshot_senior_bal,
-                pool.junior_fee_mult_bps(),
-                fee_delta,
-            );
-            // Credit junior sub-pool with its share. Senior implicitly receives
-            // the remainder (fee_delta - junior_fee) since senior_balance is derived
-            // as total_pool_value() - junior_balance and total_fees_earned was already
-            // incremented by the full fee_delta above.
-            pool.set_junior_balance(
-                pool.junior_balance()
-                    .checked_add(junior_fee)
-                    .ok_or(StakeError::Overflow)?,
-            );
-        }
-
-        msg!(
-            "AccrueFees: accrued {} fees, total_fees_earned={}",
-            fee_delta,
-            pool.total_fees_earned
-        );
-    }
+    // #136: fold any un-accrued vault surplus into share price via the shared helper,
+    // so this permissionless instruction and the deposit/withdraw pre-accrue guard apply
+    // byte-identical accounting (snapshot-before-increment + tranche distribution).
+    accrue_fees_inner(pool, current_balance)?;
 
     pool.last_fee_accrual_slot = clock.slot;
     pool.last_vault_snapshot = current_balance;
diff --git a/tests/poc_jit_fee_snipe.rs b/tests/poc_jit_fee_snipe.rs
new file mode 100644
index 0000000..82acbc9
--- /dev/null
+++ b/tests/poc_jit_fee_snipe.rs
@@ -0,0 +1,129 @@
+//! PoC / regression — JIT fee-snipe on trading-LP (mode 1) pools.
+//!
+//! ── The bug ──────────────────────────────────────────────────────────────────
+//! Trading fees are paid into the stake vault by the engine and sit there as an
+//! UN-ACCRUED surplus (`current_balance > total_pool_value()`) until someone calls
+//! the PERMISSIONLESS `AccrueFees`, which folds the whole surplus into
+//! `total_fees_earned` (`processor.rs:1688-1690`), lifting LP share price for ALL
+//! holders. But `process_deposit` prices new LP against `total_pool_value()`
+//! (`calc_lp_for_deposit`) WITHOUT crystallizing the pending surplus first. So a
+//! depositor can buy LP at the stale pre-fee price right before accrual (or
+//! self-trigger `AccrueFees` in the same tx) and capture a pro-rata share of fees
+//! earned BEFORE they joined — diluting the LPs who actually earned them.
+//!
+//! These tests model the vault token balance (`vault`) alongside the pool ledger
+//! and apply the EXACT formulas the program uses: `AccrueFees` =
+//! `total_fees_earned += vault - total_pool_value()` (guarded `vault > pv &&
+//! supply > 0`); deposit pricing = `calc_lp_for_deposit(total_lp_supply,
+//! total_pool_value(), amount)`; withdraw = `calc_collateral_for_withdraw(...)`.
+
+use bytemuck::Zeroable;
+use percolator_stake::state::StakePool;
+
+fn mode1_pool() -> StakePool {
+    let mut pool = StakePool::zeroed();
+    pool.is_initialized = 1;
+    pool.bump = 255;
+    pool.vault_authority_bump = 254;
+    pool.admin_transferred = 1;
+    pool.pool_mode = 1; // trading LP pool
+    pool.set_discriminator();
+    pool
+}
+
+/// Models `AccrueFees`: fold the vault surplus into total_fees_earned.
+fn accrue(pool: &mut StakePool, vault: u64) {
+    let pv = pool.total_pool_value().unwrap();
+    if vault > pv && pool.total_lp_supply > 0 {
+        pool.total_fees_earned += vault - pv;
+    }
+}
+
+/// Models the CURRENT `process_deposit`: price against total_pool_value() (no pre-accrue).
+fn deposit_current(pool: &mut StakePool, vault: &mut u64, amount: u64) -> u64 {
+    let lp = pool.calc_lp_for_deposit(amount).expect("calc_lp_for_deposit");
+    pool.total_deposited += amount;
+    pool.total_lp_supply += lp;
+    *vault += amount;
+    lp
+}
+
+/// Models a FIXED `process_deposit`: crystallize pending fees BEFORE pricing.
+fn deposit_fixed(pool: &mut StakePool, vault: &mut u64, amount: u64) -> u64 {
+    accrue(pool, *vault); // <-- the fix: fold pending surplus into share price first
+    let lp = pool.calc_lp_for_deposit(amount).expect("calc_lp_for_deposit");
+    pool.total_deposited += amount;
+    pool.total_lp_supply += lp;
+    *vault += amount;
+    lp
+}
+
+fn withdraw(pool: &mut StakePool, vault: &mut u64, lp: u64) -> u64 {
+    let coll = pool.calc_collateral_for_withdraw(lp).expect("calc_collateral_for_withdraw");
+    pool.total_withdrawn += coll;
+    pool.total_lp_supply -= lp;
+    *vault -= coll;
+    coll
+}
+
+#[test]
+fn jit_fee_snipe_is_profitable_with_current_pricing() {
+    let mut pool = mode1_pool();
+    let mut vault = 0u64;
+
+    // Honest LP Alice is the sole holder while 1,000,000 of fees are earned.
+    let alice_lp = deposit_current(&mut pool, &mut vault, 1_000_000);
+    vault += 1_000_000; // engine pays in trading fees (un-accrued surplus)
+
+    // Eve front-runs the accrual: deposits at the STALE pre-fee price...
+    let eve_dep = 1_000_000u64;
+    let eve_lp = deposit_current(&mut pool, &mut vault, eve_dep);
+    // ...then anyone calls AccrueFees (Eve can do it in the same tx).
+    accrue(&mut pool, vault);
+    let eve_back = withdraw(&mut pool, &mut vault, eve_lp);
+
+    assert!(
+        eve_back > eve_dep,
+        "JIT snipe must profit (got {eve_back} for {eve_dep})"
+    );
+
+    // The profit is taken from Alice's earned fees: her fair outcome (sole LP) was
+    // 1,000,000 deposit + 1,000,000 fees = 2,000,000; she now gets less.
+    let alice_back = withdraw(&mut pool, &mut vault, alice_lp);
+    assert!(
+        alice_back < 2_000_000,
+        "Alice was diluted out of fees she earned (got {alice_back}, fair 2,000,000)"
+    );
+    assert_eq!(
+        (eve_back - eve_dep) + (alice_back - 1_000_000),
+        1_000_000,
+        "Eve's gain + Alice's gain == total fees (Eve captured part of Alice's earnings)"
+    );
+}
+
+#[test]
+fn crystallizing_fees_before_pricing_prevents_snipe() {
+    // Regression guard for the fix direction: accrue pending fees BEFORE pricing a
+    // deposit. The JIT depositor then buys at the post-fee price and gains nothing;
+    // the honest LP keeps the full fees she earned.
+    let mut pool = mode1_pool();
+    let mut vault = 0u64;
+
+    let alice_lp = deposit_fixed(&mut pool, &mut vault, 1_000_000);
+    vault += 1_000_000; // fees earned while Alice is sole LP
+
+    let eve_dep = 1_000_000u64;
+    let eve_lp = deposit_fixed(&mut pool, &mut vault, eve_dep); // pre-accrues -> fair price
+    accrue(&mut pool, vault);
+    let eve_back = withdraw(&mut pool, &mut vault, eve_lp);
+    assert!(
+        eve_back <= eve_dep,
+        "FIX: JIT depositor must not profit (got {eve_back} for {eve_dep})"
+    );
+
+    let alice_back = withdraw(&mut pool, &mut vault, alice_lp);
+    assert!(
+        alice_back >= 2_000_000,
+        "FIX: honest LP keeps the fees she earned (got {alice_back})"
+    );
+}
diff --git a/tests/poc_senior_bootstrap_orphan.rs b/tests/poc_senior_bootstrap_orphan.rs
new file mode 100644
index 0000000..e196715
--- /dev/null
+++ b/tests/poc_senior_bootstrap_orphan.rs
@@ -0,0 +1,191 @@
+//! Regression test for the senior-tranche bootstrap C9-bypass.
+//!
+//! ── The regression (in the first cut of the senior sub-pool pricing fix) ───────
+//! The senior deposit path special-cased `senior_total_lp() == 0` into an
+//! UNCONDITIONAL 1:1 bootstrap (`if senior_lp == 0 { lp_to_mint = amount }`),
+//! intending to seed the first senior depositor. But that branch never consulted
+//! the orphaned-value (C9) guard that the global/junior paths use. The exact C9
+//! state — all LP withdrawn (`total_lp_supply == 0`) after insurance was returned
+//! (`total_returned > 0`, so `total_pool_value() > 0`) — yields `senior_total_lp()
+//! == 0` *with* `senior_balance() > 0`. In a tranche pool that routed into the
+//! unguarded bootstrap, so a 1-token deposit minted 1 senior LP against the whole
+//! orphaned balance and redeemed it: direct theft of returned insurance.
+//!
+//! (On the merged code this was additionally gated by the `market_resolved` deposit
+//! check, making it latent rather than live; this guard removes the dependence on
+//! that single unrelated control and restores the C9 invariant the proofs certify.)
+//!
+//! ── The fix ──────────────────────────────────────────────────────────────────
+//! `process_deposit` no longer special-cases `senior_total_lp() == 0`. It ALWAYS
+//! calls `calc_senior_lp_for_deposit(senior_total_lp(), senior_balance(), amount)`,
+//! which delegates to `calc_lp_for_deposit` and therefore inherits C9: a TRUE first
+//! senior (`senior_balance == 0`) mints 1:1, while ORPHANED senior value
+//! (`senior_balance > 0` with no senior LP) returns `None` → the deposit is rejected
+//! exactly as the non-tranche path rejects it.
+//!
+//! State/math-level, no Solana runtime — exercises the exact functions the processor
+//! calls, mirroring `tests/integration.rs` and `poc_senior_deposit_mispricing.rs`.
+
+use bytemuck::Zeroable;
+use percolator_stake::math::{calc_senior_collateral_for_withdraw, calc_senior_lp_for_deposit};
+use percolator_stake::state::StakePool;
+
+fn initialized_pool() -> StakePool {
+    let mut pool = StakePool::zeroed();
+    pool.is_initialized = 1;
+    pool.bump = 255;
+    pool.vault_authority_bump = 254;
+    pool.admin_transferred = 1;
+    pool.set_discriminator();
+    pool
+}
+
+/// A tranche pool holding 500k ORPHANED value with zero LP outstanding.
+///
+/// Reached by: senior deposited 1M → 500k flushed to insurance → senior fully
+/// exited (withdrew the remaining 500k, `total_lp_supply → 0`) → 500k insurance
+/// returned post-resolution (`total_returned += 500k`). Net pool value is 500k but
+/// no LP token has a claim on it.
+fn orphan_pool() -> StakePool {
+    let mut pool = initialized_pool();
+    pool.set_tranche_enabled(true);
+    pool.total_deposited = 1_000_000;
+    pool.total_withdrawn = 500_000;
+    pool.total_flushed = 500_000;
+    pool.total_returned = 500_000;
+    // total_lp_supply / junior_balance / junior_total_lp stay 0 (zeroed defaults).
+    pool
+}
+
+#[test]
+fn orphan_state_is_well_formed() {
+    let pool = orphan_pool();
+    assert_eq!(pool.total_lp_supply, 0, "all LP exited");
+    assert_eq!(pool.senior_total_lp(), 0, "no senior LP");
+    assert_eq!(pool.effective_junior_balance(), 0, "no junior; net_loss == 0");
+    assert_eq!(pool.total_pool_value().unwrap(), 500_000, "orphaned value present");
+    assert_eq!(
+        pool.senior_balance().unwrap(),
+        500_000,
+        "senior_total_lp == 0 while senior_balance > 0 — the orphan signature"
+    );
+}
+
+#[test]
+fn unconditional_bootstrap_was_a_c9_bypass() {
+    // Documents the regression: the OLD `if senior_lp == 0 { amount }` bootstrap.
+    let mut pool = orphan_pool();
+    let attacker_dep = 1u64;
+
+    // OLD behavior: seed 1:1 regardless of the 500k orphan sitting in the pool.
+    let minted_lp = attacker_dep;
+    pool.total_deposited += attacker_dep;
+    pool.total_lp_supply += minted_lp;
+
+    // Attacker is now the SOLE senior LP, valued against the whole senior sub-pool.
+    let coll = calc_senior_collateral_for_withdraw(
+        pool.senior_total_lp(),
+        pool.senior_balance().unwrap(),
+        minted_lp,
+    )
+    .expect("senior withdraw");
+
+    assert_eq!(coll, 500_001, "redeems the orphan plus the 1-token deposit");
+    assert_eq!(
+        coll - attacker_dep,
+        500_000,
+        "REGRESSION: a 1-token deposit drains the entire orphaned balance"
+    );
+}
+
+#[test]
+fn c9_guard_rejects_senior_deposit_into_orphan() {
+    // FIX: process_deposit now ALWAYS routes through calc_senior_lp_for_deposit,
+    // which returns None for the orphan state — the deposit is rejected (Overflow).
+    let pool = orphan_pool();
+
+    assert_eq!(
+        calc_senior_lp_for_deposit(pool.senior_total_lp(), pool.senior_balance().unwrap(), 1),
+        None,
+        "FIX: dust deposit into an orphan must be rejected (C9), not bootstrapped 1:1"
+    );
+    // It is the STATE that is blocked, not a size threshold — any amount is rejected.
+    assert_eq!(
+        calc_senior_lp_for_deposit(pool.senior_total_lp(), pool.senior_balance().unwrap(), 1_000_000),
+        None,
+        "FIX: a large deposit into an orphan is rejected too"
+    );
+}
+
+#[test]
+fn first_senior_deposit_into_empty_pool_mints_1_to_1() {
+    // No-brick guard: a TRUE first senior (empty pool, senior_balance == 0) must
+    // still mint 1:1 — the C9 guard only fires when senior_balance > 0.
+    let mut pool = initialized_pool();
+    pool.set_tranche_enabled(true);
+    assert_eq!(pool.senior_total_lp(), 0);
+    assert_eq!(pool.senior_balance().unwrap(), 0);
+
+    let lp = calc_senior_lp_for_deposit(pool.senior_total_lp(), pool.senior_balance().unwrap(), 750_000)
+        .expect("FIX: true first senior into an empty pool must succeed");
+    assert_eq!(lp, 750_000, "true first senior mints 1:1");
+}
+
+#[test]
+fn first_senior_after_junior_only_mints_1_to_1() {
+    // No-brick guard: junior deposited first, no senior yet. In mode 0 (and mode 1,
+    // where junior captures 100% of fees) this leaves senior_balance == 0, so the
+    // first senior still mints 1:1 — NOT rejected, NOT bypassed.
+    let mut pool = initialized_pool();
+    pool.set_tranche_enabled(true);
+    pool.set_junior_balance(1_000_000);
+    pool.set_junior_total_lp(1_000_000);
+    pool.total_deposited = 1_000_000;
+    pool.total_lp_supply = 1_000_000;
+    assert_eq!(pool.senior_total_lp(), 0);
+    assert_eq!(
+        pool.senior_balance().unwrap(),
+        0,
+        "junior-first leaves senior_balance == 0 (not an orphan)"
+    );
+
+    let lp = calc_senior_lp_for_deposit(pool.senior_total_lp(), pool.senior_balance().unwrap(), 500_000)
+        .expect("FIX: first senior after junior-only must succeed");
+    assert_eq!(lp, 500_000, "first senior mints 1:1");
+}
+
+#[test]
+fn junior_only_with_partial_loss_first_senior_not_bricked() {
+    // The subtle case: a junior-only pool that took a loss WITH an intervening junior
+    // withdrawal, then a partial recovery. Because no senior ever deposited,
+    // gross_senior = (total_deposited - total_withdrawn) - junior_balance stays 0, so
+    // the junior absorbs 100% of net_loss (senior_loss == 0) and senior_balance stays
+    // exactly 0 throughout. The first senior therefore still mints 1:1 — NOT rejected.
+    // (And even if some exotic state produced a phantom senior_balance > 0 with no
+    // senior LP, the fix would REJECT it — fail-safe, never a mint-orphan/theft.)
+    //
+    // State: junior deposited 1M, withdrew 200k (1:1, pre-loss), then 300k flushed,
+    // then 100k returned -> net_loss = 200k (<= junior_balance 800k).
+    let mut pool = initialized_pool();
+    pool.set_tranche_enabled(true);
+    pool.set_junior_balance(800_000); // 1M deposited - 200k withdrawn
+    pool.set_junior_total_lp(800_000);
+    pool.total_deposited = 1_000_000;
+    pool.total_withdrawn = 200_000;
+    pool.total_flushed = 300_000;
+    pool.total_returned = 100_000;
+    pool.total_lp_supply = 800_000; // all junior
+
+    assert_eq!(pool.senior_total_lp(), 0);
+    assert_eq!(pool.effective_junior_balance(), 600_000, "junior absorbs all net_loss");
+    assert_eq!(pool.total_pool_value().unwrap(), 600_000);
+    assert_eq!(
+        pool.senior_balance().unwrap(),
+        0,
+        "junior-only (gross_senior == 0) keeps senior_balance == 0 through loss + recovery"
+    );
+
+    let lp = calc_senior_lp_for_deposit(pool.senior_total_lp(), pool.senior_balance().unwrap(), 400_000)
+        .expect("FIX: first senior into a junior-only-post-loss pool must succeed 1:1");
+    assert_eq!(lp, 400_000, "first senior mints 1:1 (not bricked by a phantom senior_balance)");
+}
diff --git a/tests/poc_senior_deposit_mispricing.rs b/tests/poc_senior_deposit_mispricing.rs
new file mode 100644
index 0000000..d4d2092
--- /dev/null
+++ b/tests/poc_senior_deposit_mispricing.rs
@@ -0,0 +1,144 @@
+//! Regression test for the senior LP deposit/withdraw pricing asymmetry.
+//!
+//! ── The bug (fixed) ──────────────────────────────────────────────────────────
+//! With tranches enabled, a SENIOR deposit used to mint LP at the GLOBAL price
+//! (`process_deposit` → `StakePool::calc_lp_for_deposit`), while a SENIOR withdraw
+//! redeems at the SENIOR SUB-POOL price (`math::calc_senior_collateral_for_withdraw`).
+//! After a junior-absorbed loss (`total_flushed > total_returned`) the global price
+//! falls below the senior price, so an unprivileged user could mint senior LP cheap
+//! (global) and redeem dear (senior), extracting value from existing senior LPs.
+//!
+//! ── The fix ──────────────────────────────────────────────────────────────────
+//! `process_deposit` now prices senior deposits against the senior sub-pool via
+//! `math::calc_senior_lp_for_deposit(senior_total_lp(), senior_balance(), amount)`
+//! when `tranche_enabled()`. The first-senior deposit AND the orphaned-value (C9)
+//! guard are handled inside that helper (it delegates to `calc_lp_for_deposit`): a
+//! true first senior (`senior_balance == 0`) mints 1:1, while orphaned senior value
+//! (`senior_total_lp == 0 && senior_balance > 0`) is REJECTED. This mirrors the
+//! junior deposit path and the senior withdraw path. See `poc_senior_bootstrap_orphan`
+//! for the orphan-rejection regression guard.
+//!
+//! These tests model deposits/withdrawals on the pool struct exactly as the repo's
+//! `tests/integration.rs` does (no runtime), exercising the same functions the
+//! processor calls. `global_pricing_was_exploitable` documents the original bug;
+//! the other two are the regression guards for the fix.
+
+use bytemuck::Zeroable;
+use percolator_stake::math::{calc_senior_collateral_for_withdraw, calc_senior_lp_for_deposit};
+use percolator_stake::state::StakePool;
+
+fn initialized_pool() -> StakePool {
+    let mut pool = StakePool::zeroed();
+    pool.is_initialized = 1;
+    pool.bump = 255;
+    pool.vault_authority_bump = 254;
+    pool.admin_transferred = 1;
+    pool.set_discriminator();
+    pool
+}
+
+/// Old (buggy) senior deposit pricing: GLOBAL pool ratio.
+fn senior_deposit_global(pool: &mut StakePool, amount: u64) -> u64 {
+    let lp = pool.calc_lp_for_deposit(amount).expect("calc_lp_for_deposit");
+    pool.total_deposited += amount;
+    pool.total_lp_supply += lp;
+    lp
+}
+
+/// Fixed senior deposit pricing — mirrors the post-fix `process_deposit` tranche
+/// branch: ALWAYS prices against the senior sub-pool via `calc_senior_lp_for_deposit`,
+/// with NO special-case `senior_total_lp() == 0` bootstrap. The helper handles the
+/// true first senior (`senior_balance == 0` → 1:1) and rejects orphaned senior value
+/// (`senior_balance > 0` with no senior LP) itself. `.expect()` here only covers the
+/// legitimate (non-orphan) states these tests build; orphan rejection is exercised in
+/// `poc_senior_bootstrap_orphan`.
+fn senior_deposit_fixed(pool: &mut StakePool, amount: u64) -> u64 {
+    let senior_lp = pool.senior_total_lp();
+    let senior_bal = pool.senior_balance().expect("senior_balance");
+    let lp = calc_senior_lp_for_deposit(senior_lp, senior_bal, amount)
+        .expect("calc_senior_lp_for_deposit");
+    pool.total_deposited += amount;
+    pool.total_lp_supply += lp;
+    lp
+}
+
+/// Senior withdraw — same as `process_withdraw`'s senior branch.
+fn senior_withdraw(pool: &mut StakePool, lp: u64) -> u64 {
+    let coll = calc_senior_collateral_for_withdraw(pool.senior_total_lp(), pool.senior_balance().unwrap(), lp)
+        .expect("calc_senior_collateral_for_withdraw");
+    pool.total_withdrawn += coll;
+    pool.total_lp_supply -= lp;
+    coll
+}
+
+/// Tranche pool: junior 1M + honest senior "Alice" 1M, then a junior-absorbed 800k loss.
+fn setup() -> (StakePool, u64) {
+    let mut pool = initialized_pool();
+    pool.set_tranche_enabled(true);
+    pool.set_junior_balance(1_000_000);
+    pool.set_junior_total_lp(1_000_000);
+    pool.total_deposited += 1_000_000;
+    pool.total_lp_supply += 1_000_000;
+    let alice_lp = senior_deposit_global(&mut pool, 1_000_000); // first senior: 1:1 regardless
+    pool.total_flushed = 800_000;
+    // Junior absorbed the loss; the two price bases now diverge (global 0.6 < senior 1.0).
+    assert_eq!(pool.effective_junior_balance(), 200_000);
+    assert_eq!(pool.senior_balance().unwrap(), 1_000_000);
+    (pool, alice_lp)
+}
+
+#[test]
+fn global_pricing_was_exploitable() {
+    // Documents the original vulnerability: with the OLD global-priced senior
+    // deposit, an unprivileged user profits at existing seniors' expense.
+    let (mut pool, _alice_lp) = setup();
+    let eve_dep = 1_000_000u64;
+    let eve_lp = senior_deposit_global(&mut pool, eve_dep);
+    let eve_back = senior_withdraw(&mut pool, eve_lp);
+    assert!(
+        eve_back > eve_dep,
+        "global pricing must reproduce the exploit (got {eve_back} for {eve_dep})"
+    );
+}
+
+#[test]
+fn senior_subpool_pricing_prevents_extraction() {
+    // Regression guard: the FIXED senior sub-pool pricing yields NO profit and
+    // leaves the incumbent senior whole.
+    let (mut pool, alice_lp) = setup();
+    let alice_before =
+        calc_senior_collateral_for_withdraw(pool.senior_total_lp(), pool.senior_balance().unwrap(), alice_lp).unwrap();
+
+    let eve_dep = 1_000_000u64;
+    let eve_lp = senior_deposit_fixed(&mut pool, eve_dep);
+    let eve_back = senior_withdraw(&mut pool, eve_lp);
+    assert!(
+        eve_back <= eve_dep,
+        "FIX: sub-pool-priced senior deposit must not profit (got {eve_back} for {eve_dep})"
+    );
+
+    let alice_after =
+        calc_senior_collateral_for_withdraw(pool.senior_total_lp(), pool.senior_balance().unwrap(), alice_lp).unwrap();
+    assert!(
+        alice_after >= alice_before,
+        "FIX: incumbent senior must not be diluted ({alice_before} -> {alice_after})"
+    );
+}
+
+#[test]
+fn bootstrap_first_senior_deposit_does_not_brick() {
+    // First senior deposit into a junior-only pool (senior_total_lp == 0,
+    // senior_balance == 0) must succeed 1:1 via the helper's first-depositor path
+    // — NOT be rejected by the orphaned-value guard (which only fires when
+    // senior_balance > 0). A legitimate first senior must not be bricked.
+    let mut pool = initialized_pool();
+    pool.set_tranche_enabled(true);
+    pool.set_junior_balance(1_000_000);
+    pool.set_junior_total_lp(1_000_000);
+    pool.total_deposited += 1_000_000;
+    pool.total_lp_supply += 1_000_000;
+    assert_eq!(pool.senior_total_lp(), 0);
+
+    let lp = senior_deposit_fixed(&mut pool, 500_000);
+    assert_eq!(lp, 500_000, "first senior deposit bootstraps 1:1");
+}
diff --git a/tests/proptest_math.rs b/tests/proptest_math.rs
index dfd5e3e..7551560 100644
--- a/tests/proptest_math.rs
+++ b/tests/proptest_math.rs
@@ -6,6 +6,15 @@
 
 use proptest::prelude::*;
 
+// Tranche tests below call the REAL production functions directly (not local
+// mirrors), so they cannot drift from production. See the "Tranche math" section.
+use percolator_stake::math::{
+    calc_junior_collateral_for_withdraw, calc_junior_lp_for_deposit,
+    calc_senior_collateral_for_withdraw, calc_senior_lp_for_deposit, distribute_fees,
+    distribute_loss,
+};
+use percolator_stake::state::StakePool;
+
 // Mirror production functions exactly (from src/math.rs)
 fn calc_lp_for_deposit(supply: u64, pool_value: u64, deposit: u64) -> Option<u64> {
     // C9 fix: block deposits when orphaned value or valueless LP exists
@@ -312,3 +321,165 @@ fn test_three_depositors_sequential_conservation() {
     assert_eq!(c_back + b_back + a_back, 350);
     assert!(c_back + b_back + a_back <= 100 + 200 + 50);
 }
+
+// ═══════════════════════════════════════════════════════════════
+// Tranche math (senior/junior sub-pools, loss & fee distribution,
+// tranche valuation). Calls the REAL production functions in
+// `percolator_stake::math` and `percolator_stake::state::StakePool` — the
+// u64 property-test complement to the §15 Kani proofs.
+// ═══════════════════════════════════════════════════════════════
+
+/// Build a mode-0 (insurance LP) tranche pool with the given ledger fields.
+fn tranche_pool(deposited: u64, withdrawn: u64, flushed: u64, returned: u64, junior_balance: u64) -> StakePool {
+    use bytemuck::Zeroable;
+    let mut pool = StakePool::zeroed();
+    pool.is_initialized = 1;
+    pool.set_discriminator();
+    pool.set_tranche_enabled(true);
+    pool.total_deposited = deposited;
+    pool.total_withdrawn = withdrawn;
+    pool.total_flushed = flushed;
+    pool.total_returned = returned;
+    pool.set_junior_balance(junior_balance);
+    pool // pool_mode 0
+}
+
+proptest! {
+    // ── Loss distribution: junior absorbs first, value conserved ──
+
+    #[test]
+    fn prop_distribute_loss_conservation(
+        jb in 0u64..1_000_000_000,
+        sb in 0u64..1_000_000_000,
+        loss in 0u64..2_000_000_000u64,
+    ) {
+        let (jl, sl) = distribute_loss(jb, sb, loss);
+        let capped = loss.min(jb + sb);
+        prop_assert_eq!(jl + sl, capped, "loss not conserved");
+        prop_assert!(jl <= jb, "junior over-charged");
+        prop_assert!(sl <= sb, "senior over-charged");
+    }
+
+    #[test]
+    fn prop_distribute_loss_junior_first(
+        jb in 0u64..1_000_000_000,
+        sb in 0u64..1_000_000_000,
+        loss in 0u64..1_000_000_000u64,
+    ) {
+        prop_assume!(loss <= jb);
+        let (jl, sl) = distribute_loss(jb, sb, loss);
+        prop_assert_eq!(sl, 0, "senior took loss while junior could absorb");
+        prop_assert_eq!(jl, loss);
+    }
+
+    // ── Fee distribution: conserved, junior captures all when no senior ──
+
+    #[test]
+    fn prop_distribute_fees_conservation(
+        jb in 0u64..1_000_000_000,
+        sb in 0u64..1_000_000_000,
+        mult in 1u16..50_000,
+        fee in 0u64..1_000_000_000u64,
+    ) {
+        let (jf, sf) = distribute_fees(jb, sb, mult, fee);
+        prop_assert!(jf <= fee);
+        prop_assert!(jf + sf <= fee, "fees exceed total");
+        if fee > 0 && (jb > 0 || sb > 0) {
+            prop_assert_eq!(jf + sf, fee, "fee not fully conserved when distributable");
+        }
+    }
+
+    #[test]
+    fn prop_distribute_fees_no_senior_all_to_junior(
+        jb in 1u64..1_000_000_000,
+        mult in 1u16..50_000,
+        fee in 1u64..1_000_000_000u64,
+    ) {
+        let (jf, sf) = distribute_fees(jb, 0, mult, fee);
+        prop_assert_eq!(jf, fee, "junior should capture all fees when no senior tranche");
+        prop_assert_eq!(sf, 0);
+    }
+
+    // ── Sub-pool deposit guard (C9) + first-depositor 1:1 ──
+
+    #[test]
+    fn prop_subpool_deposit_orphan_blocked(
+        bal in 1u64..1_000_000_000,
+        dep in 1u64..1_000_000_000u64,
+    ) {
+        // sub_lp == 0 but sub_balance > 0 => orphaned value => rejected (not 1:1).
+        prop_assert!(calc_senior_lp_for_deposit(0, bal, dep).is_none());
+        prop_assert!(calc_junior_lp_for_deposit(0, bal, dep).is_none());
+    }
+
+    #[test]
+    fn prop_subpool_first_deposit_one_to_one(dep in 1u64..1_000_000_000u64) {
+        prop_assert_eq!(calc_senior_lp_for_deposit(0, 0, dep), Some(dep));
+        prop_assert_eq!(calc_junior_lp_for_deposit(0, 0, dep), Some(dep));
+    }
+
+    // ── Sub-pool deposit→withdraw round-trip cannot profit ──
+
+    #[test]
+    fn prop_senior_roundtrip_no_profit(
+        slp in 1u64..1_000_000_000,
+        sbal in 1u64..1_000_000_000,
+        dep in 1u64..1_000_000_000u64,
+    ) {
+        let lp = match calc_senior_lp_for_deposit(slp, sbal, dep) {
+            Some(l) if l > 0 => l, _ => return Ok(()),
+        };
+        let ns = match slp.checked_add(lp) { Some(v) => v, None => return Ok(()) };
+        let nb = match sbal.checked_add(dep) { Some(v) => v, None => return Ok(()) };
+        let back = match calc_senior_collateral_for_withdraw(ns, nb, lp) {
+            Some(v) => v, None => return Ok(()),
+        };
+        prop_assert!(back <= dep, "senior round-trip profited: {} > {}", back, dep);
+    }
+
+    #[test]
+    fn prop_junior_roundtrip_no_profit(
+        jlp in 1u64..1_000_000_000,
+        jbal in 1u64..1_000_000_000,
+        dep in 1u64..1_000_000_000u64,
+    ) {
+        let lp = match calc_junior_lp_for_deposit(jlp, jbal, dep) {
+            Some(l) if l > 0 => l, _ => return Ok(()),
+        };
+        let ns = match jlp.checked_add(lp) { Some(v) => v, None => return Ok(()) };
+        let nb = match jbal.checked_add(dep) { Some(v) => v, None => return Ok(()) };
+        let back = match calc_junior_collateral_for_withdraw(ns, nb, lp) {
+            Some(v) => v, None => return Ok(()),
+        };
+        prop_assert!(back <= dep, "junior round-trip profited: {} > {}", back, dep);
+    }
+
+    // ── Tranche valuation never bricks senior; tranches partition the pool ──
+
+    #[test]
+    fn prop_senior_balance_never_underflows(
+        deposited in 0u64..1_000_000_000,
+        withdrawn_raw in 0u64..1_000_000_000,
+        flushed_raw in 0u64..1_000_000_000,
+        returned_raw in 0u64..1_000_000_000,
+        junior_raw in 0u64..1_000_000_000,
+    ) {
+        // Derive a VALID pool state by construction (clamp into range) rather than
+        // generate-and-reject: uniform-independent generation satisfies all four
+        // ordering constraints only rarely and trips proptest's global-reject cap.
+        let withdrawn = withdrawn_raw % (deposited + 1);
+        let gross_pool = deposited - withdrawn;
+        let flushed = flushed_raw % (gross_pool + 1);       // can't flush more than principal
+        let returned = returned_raw % (flushed + 1);        // can't return more than flushed
+        let junior_balance = junior_raw % (gross_pool + 1); // junior balance ≤ net principal
+
+        let pool = tranche_pool(deposited, withdrawn, flushed, returned, junior_balance);
+        let pv = pool.total_pool_value().unwrap();
+        let ejb = pool.effective_junior_balance();
+        prop_assert!(ejb <= pv, "effective_junior {} > pool_value {}", ejb, pv);
+
+        // senior_balance() = pv - ejb is always Some, and the split is exact.
+        let sb = pool.senior_balance().expect("senior_balance must be Some under pool invariants");
+        prop_assert_eq!(sb + ejb, pv, "tranches do not partition the pool exactly");
+    }
+}