test(tranche): Kani proofs + proptests for tranche math (close coverage gap) - #141
Closed
0x-SquidSol wants to merge 7 commits into
Closed
test(tranche): Kani proofs + proptests for tranche math (close coverage gap)#1410x-SquidSol wants to merge 7 commits into
0x-SquidSol wants to merge 7 commits into
Conversation
dcccrypto#130) effective_junior_balance is used in every junior deposit (process_deposit_junior) for LP pricing and every junior withdrawal (process_withdraw) for collateral valuation. It composes the already-Kani-proven distribute_loss with a derivation of gross_senior from raw accounting fields. The wrapper composition itself — the net_loss == 0 short-circuit, the gross_senior derivation, and the final saturating_sub — had no formal verification, despite the historical BUG-6 fix where losses were previously double-applied on the junior side. Added 4 Kani proofs to tests/kani.rs: 1. proof_effective_junior_balance_no_panic Panic-freedom across arbitrary accounting states, including pathological cases (withdrawn > deposited, flushed > returned). 2. proof_effective_junior_balance_bounded_by_raw effective_junior_balance() <= junior_balance() for all inputs. Loss adjustment can only decrease, never inflate. Includes kani::cover! guard proving the loss-application branch is reachable beyond the trivial net_loss == 0 short-circuit. 3. proof_effective_junior_balance_no_loss_identity When total_flushed == total_returned (no outstanding loss), effective == junior_balance exactly. Pins the short-circuit against regression that would silently apply non-zero loss on lossless pools. 4. proof_effective_junior_tranche_conservation effective_junior + senior_balance == total_pool_value when both are well-defined. Regression guard in case senior_balance()'s definition ever changes away from being the tpv residual. All proofs use the established 1e9 bound for CBMC tractability, matching the style of the surrounding distribute_loss and distribute_fees proofs. All are inside the #[cfg(kani)] module — no effect on normal builds. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…to#129) .cargo/audit.toml ignores RUSTSEC-2022-0093 (ed25519-dalek 1.x) and RUSTSEC-2024-0344 (curve25519-dalek 3.x) with the rationale that these crates are dev-only and never reach the BPF binary. The dependency chain (solana-keypair -> ed25519-dalek-bip32 -> dalek 1.x) is reachable only via solana-sdk which lives under [dev-dependencies]. But no CI check mechanically verifies the "dev-only" claim. If a future dep change pulled either crate into the normal dep tree, the BPF binary would ship with known-vulnerable code and CI would say nothing — the ignore rules would silently become unsafe. Added .github/workflows/audit.yml with a bpf-tree-shake job that: 1. Runs cargo tree -e normal --no-default-features (excludes dev-dependencies and build-dependencies, matching the on-chain build's actual dep surface) 2. Greps the result for ed25519-dalek v1.x and curve25519-dalek v3.x 3. Fails if either appears, with a clear error pointing to the offending audit.toml ignore Verified locally: grep patterns are version-specific — curve25519-dalek v4.1.3 is legitimately present in the normal tree via solana-program, but only v3.x has the ignored CVE, so no false positive. Runs on PR, master push, weekly schedule (catches silent regressions). NOTE: the companion `cargo audit` step (tracked separately) is blocked by upstream cargo-audit 0.21.x lacking CVSS 4.0 parser support. Will be added when a fixed cargo-audit is released to crates.io. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
process_admin_set_tranche_config allowed the admin to change junior_fee_mult_bps at any time, even while junior LPs were deposited. Since process_accrue_fees reads the multiplier live (no per-epoch snapshot), a mid-life change immediately rewrites the fee split for every junior LP. Attack path: 1. Juniors deposit at multiplier M_1 2. Vault accumulates trading fees 3. Admin bumps multiplier to M_2 > M_1 4. Anyone calls AccrueFees — junior sub-pool captures outsized share 5. Admin (holding a junior position) withdraws at inflated value 6. Admin resets multiplier to M_1 to cover tracks The inverse also works: admin depresses the multiplier to silently reduce junior yield below what depositors were promised at deposit time. Fix: block any multiplier change when junior_total_lp() > 0. Idempotent re-writes (same value) still succeed so admin tooling can reapply config. Once all juniors withdraw (junior_total_lp back to 0), the multiplier is freely configurable for the next cohort. The "no disable" issue (set_tranche_enabled always hardcoded true) is left as-is — it's a design limitation, but because the current code cannot disable tranches, the related "disable mid-flight" attack surface that Agents A/C raised does not exist in practice. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…cccrypto#126) process_admin_set_insurance_policy forwarded a caller-supplied authority: Pubkey to wrapper Tag 22 without any validation. A malicious admin could set authority = their_wallet_key, causing the wrapper to record their wallet as the policy authority. They could then bypass the stake program entirely by calling the wrapper's WithdrawInsuranceLimited directly (Tag 23), signing as themselves. Funds extract to the attacker while pool.total_returned is NEVER incremented — process_admin_withdraw_insurance (the only path that updates total_returned) is skipped entirely. This silently desyncs total_pool_value() from the vault's actual balance. LP holders see no on-chain anomaly until they try to redeem against a pool whose accounting claims the funds are still in insurance, but the tokens are in the attacker's wallet. Fix: derive the expected vault_auth PDA and require the caller-supplied authority to equal it. This mirrors the exact check already present in process_admin_withdraw_insurance (lines 1418-1422). Non-breaking ABI change — the parameter is retained, just now validated. The vault_auth PDA is the ONLY signer the stake program can produce for WithdrawInsuranceLimited, so any other authority value breaks the program's own withdrawal path while enabling the bypass. There is no legitimate alternate value. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
With tranches enabled, process_deposit minted senior LP at the GLOBAL pool price while senior withdrawals redeem at the SENIOR sub-pool price. After the junior tranche absorbs an insurance loss (total_flushed > total_returned) the global per-LP price falls below the senior per-LP price, so an unprivileged user could mint senior LP cheap (global) and redeem dear (senior), extracting value from existing senior LP holders and the junior first-loss buffer. Price senior deposits via math::calc_senior_lp_for_deposit(senior_total_lp(), senior_balance(), amount) when tranche_enabled() — the same basis the senior withdraw path uses (calc_senior_collateral_for_withdraw) and symmetric with the junior deposit path. A senior_total_lp() == 0 first-depositor 1:1 bootstrap avoids bricking the senior tranche when junior deposited first and a fee/loss left orphaned senior value with zero senior LP. No state-layout change, no ABI change, no new error variants; senior accounting remains fully derived from the global counters. Adds tests/poc_senior_deposit_mispricing.rs (regression: old global pricing is exploitable; sub-pool pricing is not; bootstrap does not brick) and math unit tests for calc_senior_lp_for_deposit. Refs dcccrypto#134 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…conditional bootstrap The senior deposit path special-cased `senior_total_lp() == 0` into an unconditional 1:1 mint, which bypassed the orphaned-value (C9) guard inside `calc_lp_for_deposit`. In the reachable state where all LP has exited (`total_lp_supply == 0`) but the pool still holds value (e.g. insurance was returned post-resolution), a tranche pool has `senior_total_lp() == 0` with `senior_balance() > 0`. The bootstrap minted 1 senior LP for a 1-token deposit against the whole orphaned balance, which the depositor could then withdraw in full at the senior sub-pool price — draining the orphan. Fix: always price senior deposits via `calc_senior_lp_for_deposit` (which delegates to `calc_lp_for_deposit`), with no `senior_total_lp() == 0` special case. It mints 1:1 only for a true first senior (`senior_balance == 0`) and returns `None` for orphaned senior value (`senior_balance > 0`), rejecting the deposit exactly as the non-tranche path does. A legitimate first senior always has `senior_balance == 0` (empty pool, or a junior-first pool where junior captures 100% of fees and absorbs 100% of loss because `gross_senior == 0`), so this does not brick the first senior deposit. Adds tests/poc_senior_bootstrap_orphan.rs: reproduces the orphan-theft under the old bootstrap, asserts the fix rejects it, and proves the first senior still mints 1:1 across empty / junior-only / junior-only-post-loss-and-recovery states. Updates the existing senior-mispricing regression test to the no-bootstrap helper. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…verage gap) The formal-verification suite (kani-proofs, 44 harnesses) and proptest_math.rs covered only the GLOBAL (non-tranche) LP path. The senior/junior sub-pool pricing, loss/fee distribution, and tranche valuation — the newest, highest-risk code — had zero symbolic or property coverage, which is how the senior-deposit bootstrap regression (PR dcccrypto#135) could land undetected. Kani (kani-proofs/src/lib.rs §15, 10 new harnesses, 44 -> 54): adds u32/u64 mirrors of the tranche helpers and StakePool::{total_pool_value, effective_junior_balance, senior_balance}, and proves: - distribute_loss: conservation (jl+sl == capped loss), bounds, junior-first - distribute_fees: conservation, bounds, and no-senior => junior captures all - sub-pool C9 guard (orphaned value rejected) + true-first-depositor 1:1 - sub-pool deposit->withdraw round-trip cannot profit (senior & junior) - senior_balance never underflows (effective_junior <= pool_value) under the pool invariants (returns <= flushes, junior balance <= gross principal) - tranche decomposition: senior_balance + effective_junior == total_pool_value proptest (tests/proptest_math.rs): the u64 property-test complement, calling the REAL production functions in percolator_stake::math and StakePool directly (not local mirrors, so they cannot drift) over wide random ranges. All invariants additionally verified exhaustively (405,121 cases) against the production functions out-of-band. cargo kani + cargo test run these in CI. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Warning Review limit reached
More reviews will be available in 42 minutes and 14 seconds. Learn how PR review limits work. Your organization has used up its prepaid credits, and credit purchases are no longer available. Enable the review add-on in the billing tab to keep reviews running — you're only billed for reviews past your plan's rate limits ($0.25/file). ⌛ How to resolve this issue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based credits. 🚦 How do rate limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan refill rate. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, the refill rate gradually slows as usage increases. The highest same-day bursts are limited more strictly. Please see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (6)
✨ Finishing Touches🧪 Generate unit tests (beta)
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. Comment |
Owner
|
Proptest coverage integrated into |
dcccrypto
added a commit
that referenced
this pull request
Jun 18, 2026
…Kani (#143) (#148) * fix(stake,v17): pre-accrue mode-1 fees on the junior deposit path (#146) process_deposit_junior was the only pricing path that did not crystallize pending mode-1 trading-fee surplus before pricing — process_deposit (senior/ global) and process_withdraw already do (the #136 fix). A junior depositor could mint LP at the stale pre-fee price and, after a permissionless AccrueFees, capture a multiplier-weighted (up to 5x) share of fees earned before they joined (PoC: deposit 1,000,000 -> withdraw 1,400,000, +400,000). This is a v17-convergence drop: the original #136 fix covered all three paths. The pre-accrue block was inline-duplicated across the paths, which is how the junior copy went missing. Extract it into one shared helper pre_accrue_mode1( pool, vault) and route all three sites through it so they cannot drift again. The deposit/withdraw change is a behavior-preserving extraction (verbatim body); the junior path gets the call before pricing (after the cap/token-program/ATA checks, matching process_deposit) so it folds only the fee surplus (vault read pre-transfer) and prices against the post-accrual junior balance. Adds tests/poc_junior_jit_fee_snipe.rs (mirrors poc_jit_fee_snipe.rs): documents the +400,000 snipe under current pricing and asserts the pre-accrue neutralizes it. Verified against the v17 production functions (current 1,400,000; fixed 999,999). cargo build --lib + cargo build-sbf clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * fix(stake,v17): restore protections dropped in the v17 convergence (#143) The v17-convergence line forked before two main PRs landed and didn't re-incorporate them. Both are absent from v17; restored here. 1. junior_fee_mult_bps governance lock (originally #127): process_admin_set_tranche_config validated the multiplier range but no longer blocked changing it once junior LPs exist. process_accrue_fees reads the multiplier live (no per-epoch snapshot), so a mid-life change re-prices the junior/senior fee split for already-committed junior LPs (admin can pump before AccrueFees to extract an outsized share, or depress to cut promised junior yield). Restore: reject any change when junior_total_lp() > 0; idempotent same-value rewrites still allowed; freely configurable once all juniors exit. 2. Tranche-math Kani proofs (§15, originally part of the #140/#141 coverage): the Kani suite covered only the global path. Restore the 10 tranche harnesses + their u32/u64 mirrors: distribute_loss conservation + junior-first; distribute_fees conservation + no-senior-strands-to-junior; sub-pool C9 guard + first-depositor 1:1; sub-pool round-trip no-profit; senior_balance non-underflow; tranche decomposition. (Tranche proptests already survived.) Verification: cargo build --lib + cargo build-sbf clean; kani crate compiles; the §15 invariants verified exhaustively (405,121 cases) against the v17 production functions out-of-band; cargo kani + cargo test run them in CI. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: 0X-SquidSol <david.laszczynski@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #140.
What
Closes the tranche-math formal/property coverage gap. The Kani suite and
proptest_math.rspreviously covered only the GLOBAL (non-tranche) LP path; the senior/junior sub-pool pricing, loss/fee distribution, and tranche valuation had no symbolic or property coverage — which is how the senior-deposit bootstrap regression could land undetected.Kani (
kani-proofs/src/lib.rs, new §15 — 10 harnesses, 44 → 54): adds u32/u64 mirrors of the tranche helpers andStakePool::{total_pool_value, effective_junior_balance, senior_balance}(same scale-invariance argument as the existing global mirrors), and proves:distribute_loss: conservation (junior_loss + senior_loss == capped loss), per-tranche bounds, junior-first (senior protected).distribute_fees: bounds, conservation when distributable, and no-senior ⇒ junior captures all.senior_balance()never underflows (effective_junior_balance <= total_pool_value) under the pool invariants; tranche decomposition (senior + effective_junior == pool value).proptest (
tests/proptest_math.rs): the u64 property-test complement, calling the real production functions inpercolator_stake::mathandStakePooldirectly (not local mirrors, so they cannot drift from production).Verification
cargo build -p percolator-stake-kani: clean.cargo kaniruns the proofs in CI.cargo testruns the proptests in CI.Note — stacked on #135
The proptests reference
calc_senior_lp_for_deposit, which is introduced in #135, so this branch is based onfix/senior-deposit-subpool-pricing. Until #135 merges, this PR's diff includes #135's commits; the net-new change here is the singletest(tranche): …commit (499e4f1). Please merge #135 first (or together).