fix(stake,v17): restore junior_fee_mult_bps lock + tranche-math Kani proofs dropped in v17 convergence

[0x-SquidSol]

Closes #143.

What

Restores two protections that existed on pre-v17 main but were dropped when the v17-convergence line forked early (it pre-dated these PRs and didn't re-incorporate them). Both are absent from current v17.

1. junior_fee_mult_bps governance lock (was #127)

process_admin_set_tranche_config validated the multiplier range but no longer blocked changing it once junior LPs exist. Since process_accrue_fees reads the multiplier live (no per-epoch snapshot), a mid-life change re-prices the junior/senior fee split for already-committed junior LPs — the admin can pump it right before AccrueFees to capture an outsized share into an admin-held junior position, or depress it to silently cut promised junior yield.

Restored guard: reject any change when junior_total_lp() > 0; idempotent same-value rewrites still succeed; once all juniors exit (junior_total_lp() == 0) the multiplier is freely configurable for the next cohort.

2. Tranche-math Kani proofs (§15, was part of #140/#141)

The Kani suite covered only the global calc_lp_for_deposit/calc_collateral_for_withdraw. Restores the 10 tranche harnesses + their u32/u64 mirrors: distribute_loss conservation + junior-first; distribute_fees conservation + no-senior-strands-to-junior; sub-pool orphaned-value (C9) guard + first-depositor 1:1; sub-pool deposit→withdraw round-trip cannot profit; senior_balance never underflows; tranche decomposition. (The tranche proptests already survived the convergence; only the formal proofs were missing.)

Verification

• cargo build --lib and cargo build-sbf: clean.
• kani-proofs crate compiles; cargo kani runs the proofs in CI.
• The §15 invariants were verified exhaustively (405,121 cases) against the v17 production functions out-of-band.
• Independent review of the lock confirmed: blocks the change-with-juniors attack, allows idempotent rewrites, never bricks first-enable, fails safe under desync.

Note

The lock is a verbatim restoration of the previously-reviewed #127; #127 shipped without a unit test (it's a processor-level admin guard), so none was dropped — coverage is the build + the documented attack path + the independent review here.

Summary by CodeRabbit

• New Features

  • Added helper functions for tranche LP calculation, collateral withdrawal, and loss/fee distribution across senior and junior sub-pools.
  • Implemented governance lock: junior fee multiplier configuration is now restricted while junior LP positions exist.

• Tests

  • Expanded verification suite with 10 new proofs validating tranche deposit/withdrawal behavior, loss distribution, and pool value decomposition.

[coderabbitai]

📝 Walkthrough

Walkthrough

Restores two pre-v17 protections: process_admin_set_tranche_config now blocks changing junior_fee_mult_bps while any junior LP positions exist (returning StakeError::Unauthorized), and kani-proofs/src/lib.rs gains seven tranche math helper functions plus a new SECTION 15 with 10 Kani verification harnesses covering loss/fee distribution, sub-pool LP mechanics, and senior/junior balance decomposition.

Changes

Restore pre-v17 tranche protections

Layer / File(s)	Summary
junior_fee_mult_bps governance lock src/processor.rs	process_admin_set_tranche_config rejects any junior_fee_mult_bps change when junior_total_lp() > 0 with StakeError::Unauthorized; same-value rewrites and changes after all juniors withdraw remain allowed.
Tranche math helper functions kani-proofs/src/lib.rs	Adds calc_subpool_lp_for_deposit, calc_subpool_collateral_for_withdraw, distribute_loss, distribute_fees, total_pool_value_mode0, effective_junior_balance, and senior_balance using checked/saturating arithmetic and junior-first loss ordering.
SECTION 15 Kani harnesses kani-proofs/src/lib.rs	Adds suite description update and 10 proof harnesses: distribute_loss conservation and junior-first; distribute_fees bounds and no-senior-strands; sub-pool C9 orphaned-value rejection, first-depositor 1:1, deposit→withdraw no-profit; senior_balance no-underflow; and exact senior + effective_junior == pool_value decomposition.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~25 minutes

Possibly related PRs

• dcccrypto/percolator-stake#98: Introduced the runtime tranche fee/loss distribution logic (effective_junior_balance, distribute_fees) that the new Kani harnesses in this PR formally verify.
• dcccrypto/percolator-stake#142: Contains the distribute_fees overflow fix and tranche-aware senior pricing that the new distribute_fees proof harnesses and sub-pool C9 guard directly target.

Poem

🐇 Two guards had slipped away in the v17 tide,
A fee-mult lock and proofs that once kept tranches right inside.
Now junior LPs hold their terms—no admin sleight of hand,
And Kani harnesses stand watch, ten proofs across the land.
Conservation holds! The decomp adds up clean and true,
Senior plus effective junior equals the whole pool's view. 🌊

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly identifies the two main changes: restoring the junior_fee_mult_bps lock and the tranche-math Kani proofs, with specific issue references.
Description check	✅ Passed	The PR description thoroughly documents both protections being restored with attack vectors and fix directions, and includes verification instructions matching the template (build, clippy, format, and Kani setup).
Linked Issues check	✅ Passed	The PR successfully addresses both objectives from #143: restores the junior_fee_mult_bps governance lock in process_admin_set_tranche_config and adds 10 tranche-math Kani proof harnesses for loss/fee distribution, orphaned-value guards, and decomposition invariants.
Out of Scope Changes check	✅ Passed	All changes are directly scoped to the two stated objectives: the governance lock in processor.rs and tranche-math verification in kani-proofs/src/lib.rs with no unrelated modifications.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests

---

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

[coderabbitai]

🧹 Nitpick comments (1)

kani-proofs/src/lib.rs (1)

245-251: 💤 Low value

Minor: Proof count discrepancy in header comment.

The comment states "§15 (10 proofs)" but counting the actual harnesses in SECTION 15 yields 9 proofs. Consider updating the comment to reflect the accurate count.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@kani-proofs/src/lib.rs` around lines 245 - 251, The header comment in the
KANI PROOFS section states "§15 (10 proofs)" but the actual count of harnesses
in SECTION 15 is 9 proofs, creating a discrepancy. Update the proof count
referenced in the comment from 10 to 9 to accurately reflect the number of
proofs present in that section. This ensures the documentation remains
consistent with the actual implementation.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Nitpick comments:
In `@kani-proofs/src/lib.rs`:
- Around line 245-251: The header comment in the KANI PROOFS section states "§15
(10 proofs)" but the actual count of harnesses in SECTION 15 is 9 proofs,
creating a discrepancy. Update the proof count referenced in the comment from 10
to 9 to accurately reflect the number of proofs present in that section. This
ensures the documentation remains consistent with the actual implementation.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: e132bc64-de40-4735-ba46-79e67e888a37

📥 Commits

Reviewing files that changed from the base of the PR and between a5562ef and b119e3c.

📒 Files selected for processing (2)

• kani-proofs/src/lib.rs
• src/processor.rs

[dcccrypto]

Integrated into main via the consolidated PR above (with attribution; verified it doesn't break the admin-set-tranche tests, unlike a sibling guard PR that did). Closes #143. Thanks.