fix(stake): #200 delete dead flush_available + #194 discriminator guard + #195 ATA owner check

[dcccrypto]

Three verified findings (credit @v1ktorrr0x):

• N-1: math::flush_available() omits total_returned and uses saturating arithmetic (latent correctness trap) #200 — delete the dead, buggy math::flush_available() (no prod callers; live path uses total_pool_value() per fix(stake): compute FlushToInsurance available via total_pool_value to stop false-overflow brick #202). Removes its inline tests + the 2 kani proofs of the dead fn.
• Missing discriminator validation on already-initialized StakeDeposit accounts #194 — validate the StakeDeposit discriminator on already-init records (deposit/withdraw/deposit_junior); defense-in-depth.
• User ATA accounts not verified as SPL Token-owned before raw byte reads #195 — verify user_ata is SPL-Token-owned before raw layout reads; fail-fast vs crafted non-token accounts.

build-sbf clean, 22 test suites green. Closes #200, #194, #195.

Summary by CodeRabbit

• Bug Fixes

  • Removed buggy internal calculation code that was no longer in use.

• Security

  • Added stricter validation for token accounts and stake records to prevent unauthorized account manipulation.

• Tests

  • Updated tests to align with code changes.

[coderabbitai]

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 1a20ac7f-9f2d-4d4f-a87b-aa167468e99b

📥 Commits

Reviewing files that changed from the base of the PR and between 9fe1975 and 5ad6691.

📒 Files selected for processing (3)

• src/math.rs
• src/processor.rs
• tests/kani.rs

---

📝 Walkthrough

Walkthrough

Removes the flush_available public math helper (flagged as dead code with a wrong formula) along with its unit tests and Kani proof harnesses. Separately, adds SPL Token program ownership checks on user_ata and StakeDeposit discriminator validation in the already-initialized branches of process_deposit, process_withdraw, and process_deposit_junior.

Changes

Removal of flush_available dead code

Layer / File(s)	Summary
Remove flush_available and all proofs src/math.rs, tests/kani.rs	Deletes the flush_available function and its saturating arithmetic from src/math.rs, replacing it with a comment referencing issue #200. Removes the corresponding unit tests, the Kani panic-freedom harness, flush-bounds proof harnesses, and the flush_available import from tests/kani.rs.

Processor account validation hardening

Layer / File(s)	Summary
SPL Token ownership fail-fast checks src/processor.rs	process_deposit (line 604–610), process_withdraw (line 957–963), and process_deposit_junior (line 2419–2425) each reject user_ata before reading its raw layout if it is not owned by the SPL Token program.
StakeDeposit discriminator validation src/processor.rs	In the already-initialized branch of process_deposit (line 820–823), process_withdraw (line 1003–1006), and process_deposit_junior (line 2603–2606), the StakeDeposit discriminator is checked; an invalid discriminator returns InvalidAccount instead of proceeding.

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~12 minutes

Possibly related issues

• User ATA accounts not verified as SPL Token-owned before raw byte reads #195: The SPL Token program ownership checks added to process_deposit, process_withdraw, and process_deposit_junior implement the exact account-ownership validations prescribed by this issue.
• N-1: math::flush_available() omits total_returned and uses saturating arithmetic (latent correctness trap) #200: The removal of flush_available and its replacement with a reference to StakePool::total_pool_value() directly resolves the dead-code and incorrect-formula bug reported in this issue.

Possibly related PRs

• dcccrypto/percolator-stake#30: Added centralized account ownership/writability/initialized-state validation helpers in the same process_deposit/process_withdraw/process_deposit_junior code paths now further hardened by this PR.
• dcccrypto/percolator-stake#187: Rewrote StakePool::total_pool_value() with i128 widening to fix mode-1 underflow — the exact function this PR relies on to replace the removed flush_available capacity calculation.
• dcccrypto/percolator-stake#98: Modified process_flush_to_insurance's available-capacity computation, the same accounting area where flush_available was originally a candidate helper before being removed by this PR.

Poem

🐇 Hippity-hop, the dead code must go,
A buggy old function with saturating woe!
Now token accounts get a proper ID check,
No forged discriminators slipping through the deck.
The pool value path shines safe and bright,
This bunny approves — the math is right! 🥕

✨ 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-194-195-200

---

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.}