fix(stake): #169 — compute pool value in i128 to stop mode-1 fee-withdraw brick

[dcccrypto]

Bug (#169)

In a mode-1 trading pool, a withdrawer's payout includes their share of accrued fees, so total_withdrawn legitimately exceeds total_deposited once fees are paid out. total_pool_value()'s left-to-right total_deposited.checked_sub(total_withdrawn) then underflowed to None and permanently bricked the pool — LP funds trapped. principal_tvl() had the same shape and bricked deposits.

Fix

Sum both in a wide signed i128 intermediate (order no longer matters):

• total_pool_value() → None only when the final value is out of range (negative = genuine insolvency, or > u64::MAX). False-underflow brick gone; insolvency guard preserved. Keeps the Design: last junior exiting during an outstanding loss windfalls the recovery to senior (junior-withdraw side of #145) #161 realized_junior_loss term + PERC-272 mode-1 fee inclusion.
• principal_tvl() → clamp a net-negative basis to 0 (deposit cap admits new principal) instead of bricking. Design: last junior exiting during an outstanding loss windfalls the recovery to senior (junior-withdraw side of #145) #161 RL still excluded.

This is the i128 idea from #170 (@0x-SquidSol), reimplemented on current main so it keeps the post-#161 - realized_junior_loss() term (the PR's stale base dropped it, which would have reverted #161) and also fixes the twin principal_tvl().

Verified

• Kani proof_169_mode1_no_false_underflow_brick: i128 value == true signed sum when in range (incl. withdrawn > deposited, the bricking case) and None iff truly insolvent. 0/104 failed; cover satisfied (non-vacuous).
• Unit: 5 CRITICAL: mode-1 total_pool_value() underflows when fee-inclusive total_withdrawn exceeds total_deposited → trading pool permanently bricks (LP funds trapped) #169 regression tests; full suite green (46 + 67); build-sbf clean.

Closes #169.

🤖 Generated with Claude Code

Summary by CodeRabbit

• Bug Fixes

  • Resolved issue #169: pool value calculations no longer fail when total withdrawals exceed total deposits.
  • Improved principal value calculation accuracy in edge-case scenarios.

• Tests

  • Added unit tests for pool value calculation edge cases and fee handling verification.

[coderabbitai]

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: b574f271-6ab2-4c3b-b289-c8927c6844d9

📥 Commits

Reviewing files that changed from the base of the PR and between eb423b3 and d1fdf25.

📒 Files selected for processing (3)

• kani-proofs/src/lib.rs
• src/state.rs
• tests/unit.rs

---

📝 Walkthrough

Walkthrough

Fixes issue #169 by rewriting StakePool::total_pool_value() and principal_tvl() in src/state.rs to use i128-widened signed arithmetic, eliminating false underflow when fee-inclusive total_withdrawn exceeds total_deposited in mode-1 pools. Adds five unit tests and a Kani formal proof with a mirror helper function.

Changes

Issue #169: Mode-1 pool value i128 underflow fix

Layer / File(s)	Summary
i128 arithmetic rewrite for total_pool_value and principal_tvl src/state.rs	total_pool_value() accumulates deposited, returned, mode-1 fees, withdrawn, flushed, and realized junior loss in a single i128 signed sum, returning None only when the result is negative or exceeds u64::MAX. principal_tvl() applies the same widening but clamps negative results to Some(0) instead of None.
Unit tests for issue #169 scenarios tests/unit.rs	Five new tests assert: fee-withdrawal does not brick total_pool_value(), principal_tvl() clamps to Some(0) on net-negative principal basis, genuine insolvency still returns None, mode-0 and realized-junior-loss behavior is unchanged, and mode-1 fees appear in total value but not in principal basis.
Kani mirror helper and formal proof harness kani-proofs/src/lib.rs	Adds total_pool_value_mode1_rl_i128 using i64 signed arithmetic as a Kani-verifiable mirror, and proof_169_mode1_no_false_underflow_brick symbolically asserts the helper returns Some(true_value) on the previously bricked withdrawn > deposited path and None on genuinely negative sums.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

Possibly related PRs

• dcccrypto/percolator-stake#112: Updates calc_lp_for_deposit() to propagate None from total_pool_value(), directly coupling it to the return-value semantics changed in this PR.
• dcccrypto/percolator-stake#172: Introduces principal_tvl() and switches deposit-cap enforcement to use it, overlapping with the principal_tvl() i128 rewrite in this PR.

Poem

🐇 Hoppity-hop through the integer land,
Where i128 now lends a helping hand.
No more false None when fees tip the scale —
The pool stays solvent, deposits don't fail!
Signed arithmetic saves the LP's gold,
And Kani confirms what the proofs have told. 🎉

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/stake-169-i128-pool-value

---

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}