Standalone Insurance LP staking program for Percolator — the permissionless perpetual futures engine on Solana.
PDA-admin design — the stake program's PDA becomes the wrapper admin, enabling isolated security audits.
┌─────────────────────────────────────────────────┐
│ percolator-stake │
│ │
│ User ──► Deposit ──► Stake Vault ──► LP Mint │
│ User ◄── Withdraw ◄─ Stake Vault ◄── LP Burn │
│ │ │
│ FlushToInsurance │
│ │ │
│ CPI TopUpInsurance │
│ ▼ │
│ ┌──────────────────────────────────────────┐ │
│ │ percolator-prog (wrapper) │ │
│ │ stake_pool PDA = wrapper admin │ │
│ └──────────────────────────────────────────┘ │
└─────────────────────────────────────────────────┘
PDA derivation:
stake_pool=[b"stake_pool", slab_pubkey]— pool state + wrapper adminvault_auth=[b"vault_auth", pool_pda]— token vault authoritystake_deposit=[b"stake_deposit", pool_pda, user_pubkey]— per-user LP position
This section details all Program Derived Addresses used by the stake program.
The stake pool account holds all global state for a given slab (market).
| Property | Value |
|---|---|
| Seeds | [b"stake_pool", slab_pubkey] |
| Program ID | Stake program ID (passed in InitPool) |
| Owner | Stake program (created via CPI in InitPool) |
| Size | 472 bytes (STAKE_POOL_SIZE) |
Key Fields:
is_initialized— 1 if pool is active, 0 otherwiseadmin— Pool administrator (can call UpdateConfig, CPI admin functions)admin_transferred— 1 after TransferAdmin (required before accepting deposits)slab— The percolator market pubkey this pool managesvault— Token account holding collateral buffer (owned by vault_auth PDA)lp_mint— LP token mint (authority = vault_auth PDA)cooldown_slots— Slot delay before withdrawals allowed (must be > 0)deposit_cap— Max pool value (0 = unlimited)total_deposited,total_lp_supply,total_flushed,total_returned,total_withdrawn— Accounting totalspercolator_program— Wrapper program ID (for CPI calls)
Example derivation (Typescript using @solana/web3.js):
import { PublicKey } from '@solana/web3.js';
const programId = new PublicKey('...stake program...');
const slabPubkey = new PublicKey('...market slab...');
const [stakePoolPda, poolBump] = await PublicKey.findProgramAddress(
[Buffer.from('stake_pool'), slabPubkey.toBuffer()],
programId
);The vault authority is a PDA that owns the LP mint and vault token account. It signs all vault operations.
| Property | Value |
|---|---|
| Seeds | [b"vault_auth", stake_pool_pda] |
| Program ID | Stake program ID |
| Owner | System program (PDA has no account, just signing authority) |
| Used for | Signing mint_to, burn, transfer via invoke_signed |
Example derivation:
const [vaultAuthPda, vaultAuthBump] = await PublicKey.findProgramAddress(
[Buffer.from('vault_auth'), stakePoolPda.toBuffer()],
programId
);Each user has a deposit PDA per pool that tracks their cooldown and LP balance.
| Property | Value |
|---|---|
| Seeds | [b"stake_deposit", pool_pda, user_pubkey] |
| Program ID | Stake program ID |
| Owner | Stake program (created via CPI in Deposit) |
| Size | 120 bytes (STAKE_DEPOSIT_SIZE) |
Key Fields:
is_initialized— 1 if deposit is activepool— Back-reference to stake pool PDAuser— User pubkeylast_deposit_slot— Slot of most recent deposit (cooldown starts here)lp_amount— Total LP tokens held by this user
Example derivation:
const [depositPda, depositBump] = await PublicKey.findProgramAddress(
[Buffer.from('stake_deposit'), stakePoolPda.toBuffer(), userPubkey.toBuffer()],
programId
);LP Mint Account:
- Mint authority: vault_auth PDA (signs all mint_to and burn operations)
- Freeze authority: vault_auth PDA
- Decimals: 6
Vault Token Account (Collateral Buffer):
- Owner: vault_auth PDA
- Mint: collateral_mint (matches slab's collateral)
- Purpose: Holds collateral awaiting flushes to wrapper insurance
User Collateral ATA:
- Owner: user pubkey
- Mint: collateral_mint
- Purpose: User's collateral source/destination
User LP ATA:
- Owner: user pubkey
- Mint: lp_mint
- Purpose: User's LP token balance
| # | Instruction | Description |
|---|---|---|
| 0 | InitPool |
Create pool, LP mint, vault for a slab |
| 1 | Deposit |
User deposits tokens → vault, receives LP |
| 2 | Withdraw |
Burn LP → withdraw from vault (cooldown enforced) |
| 3 | FlushToInsurance |
Move vault tokens → wrapper insurance via CPI |
| 4 | UpdateConfig |
Admin updates cooldown period / deposit cap |
| 5 | TransferAdmin |
One-time transfer: human admin → pool PDA |
| 6 | AdminSetOracleAuthority |
CPI forward to wrapper |
| 7 | AdminSetRiskThreshold |
CPI forward to wrapper |
| 8 | AdminSetMaintenanceFee |
CPI forward to wrapper |
| 9 | AdminResolveMarket |
CPI forward to wrapper |
| 10 | AdminWithdrawInsurance |
CPI WithdrawInsuranceLimited (post-resolution) |
| 11 | AdminSetInsurancePolicy |
CPI SetInsuranceWithdrawPolicy |
- Wrapper hardening — constitutional bounds no admin can violate (PR #5)
- Stake program policies — flexible rules (cooldown, caps, flush limits) within those bounds
Security audits are fully isolated between layers.
270 tests, 0 failures. 85 Kani proof harnesses.
The percolator_program field in the StakePool account is an allowlist of authorized wrapper program IDs. Only programs on this allowlist can receive CPI calls from the stake program. This is the fix for finding F-4 (unauthorized program CPI).
Uses #[kani::unwind(33)] with u32 mirrors for CBMC tractability. Properties proven over bounded domains generalize to production u64/u128 via scale invariance.
| Category | Proofs | Key Properties |
|---|---|---|
| Conservation | 5 | Deposit→withdraw no-inflation, two-party conservation, flush+return roundtrip |
| Arithmetic Safety | 4 | Panic-freedom across full u32 input space |
| Fairness / Monotonicity | 3 | Rounding favors pool, larger deposit → more LP |
| Withdrawal Bounds | 2 | Full burn ≤ pool value, partial ≤ full |
| Flush Bounds | 2 | Flush ≤ deposited, max flush → zero remaining |
| Pool Value | 4 | Correctness, monotonicity, flush/return conservation |
| Zero Boundaries | 2 | No free LP, no free collateral |
| Cooldown | 3 | No-panic, not-immediate, exact boundary |
| Deposit Cap | 3 | Zero = uncapped, boundary precision |
| C9 Orphaned Value | 3 | All 4 LP state machine quadrants covered |
| Flush Mechanics | 2 | Exact value reduction, determinism |
| Extended Safety | 2 | Full-range panic-freedom for remaining functions |
Rating: 25 STRONG, 6 GOOD, 4 STRUCTURAL.
See docs/KANI-DEEP-ANALYSIS.md for the full proof-by-proof analysis.
| Suite | Count | Coverage |
|---|---|---|
| Math | 63 | Conservation, fairness, edge cases, large values, proptest |
| Unit | 39 | Deposit, withdraw, flush, cooldown, PDA derivation |
| Proptest | 17 | Fuzz LP math across random inputs |
| Struct Layout | 10 | Bytemuck serialization roundtrips |
| CPI Tags | 9 | All wrapper instruction tags verified |
| Error Codes | 3 | Error variant mapping |
| Integration | 129 | End-to-end program flows, percolator_program allowlist |
4 rounds of security review. Full report: docs/AUDIT.md.
| Severity | Found | Fixed |
|---|---|---|
| CRITICAL | 11 | 11 ✅ |
| HIGH | 6 | 5 ✅ |
| MEDIUM | 7 | 5 ✅ |
| LOW | 4 | 1 ✅ |
# Build BPF
cargo build-sbf
# Run tests
cargo test
# Run Kani proofs (local-only — not run in CI; see .github/workflows/kani-manual.yml for on-demand runs)
# One-time setup: cargo install --locked kani-verifier && cargo kani setup
cd kani-proofs && cargo kani --libdocs/ARCHITECTURE.md— Full architecture with CPI flow diagramsdocs/AUDIT.md— 4-round security audit reportdocs/KANI-DEEP-ANALYSIS.md— Proof-by-proof analysisdocs/WRAPPER-HARDENING.md— Wrapper foot gun limits
The BPF upgrade authority controls whether the deployed program binary can be replaced. A compromised upgrade authority key allows an attacker to deploy an arbitrary replacement program at the same program ID, bypassing all on-chain checks.
Requirement: The upgrade authority for percolator_stake.so MUST be held by an N-of-M multisig (e.g., Squads) or burned (immutable) before mainnet use.
To verify the current upgrade authority:
solana program show <PROGRAM_ID>To transfer to a multisig:
solana program set-upgrade-authority <PROGRAM_ID> --new-upgrade-authority <MULTISIG_PUBKEY>To make the program immutable (no further upgrades possible):
solana program set-upgrade-authority <PROGRAM_ID> --finalThe current deployment upgrade authority pubkey and governance process should be documented here by the maintainers.
Enforcement (#240): this requirement is gated by
scripts/check-upgrade-authority.sh — it fails CI
unless every checked program's authority is burned or held by an allowlisted governance
multisig. Full runbook (transfer-to-Squads / burn / verify):
docs/SECURITY-UPGRADE-AUTHORITY.md. The opt-in
upgrade-authority-gate workflow runs it
in CI once the UPGRADE_AUTH_* repo variables are configured.
| Repository | Description |
|---|---|
| percolator | Core risk engine crate (Rust) |
| percolator-prog | Solana on-chain program (wrapper) |
| percolator-matcher | Reference matcher program for LP pricing |
| percolator-sdk | TypeScript SDK for client integration |
| percolator-ops | Operations dashboard |
| percolator-mobile | Solana Seeker mobile trading app |
| percolator-launch | Full-stack launch platform (monorepo) |
Apache 2.0 — see LICENSE.