From 2be9682e79d0cbc310f24f6045203b5cd802cc95 Mon Sep 17 00:00:00 2001 From: Mike MacCana Date: Wed, 30 Sep 2026 16:43:19 +0000 Subject: [PATCH] Call the Kani harnesses model checks, not proofs Kani is a model checker: a harness tries every value of its declared inputs and reports that every assertion held or the input that breaks one. The docs called them formal-verification proofs. Every kani-proofs README, module doc, the program READMEs that mention them, the top-level README and the kani.yml comments now say model check, and each first mention explains that the kani-proofs and proof_* names come from Kani's #[kani::proof] attribute. No code, identifier or job name changed. Also: - "money math" becomes "arithmetic" throughout. - The lending Kani README named proof_interest_index_monotonic, which does not exist; the harness is proof_accumulation_factor_monotonic. - A token-swap comment said the harness caps each quantity at 1023; the code caps at 63. Claude-Session: https://claude.ai/code/session_01JGEoAUjMm7Evv69k46eNcn --- .github/workflows/kani.yml | 31 ++++++++------- README.md | 4 +- finance/betting-market/kani-proofs/Cargo.toml | 2 +- finance/betting-market/kani-proofs/README.md | 26 +++++++------ finance/betting-market/kani-proofs/src/lib.rs | 11 ++++-- finance/escrow/anchor-v1/README.md | 4 +- finance/escrow/anchor/README.md | 4 +- finance/escrow/kani-proofs/README.md | 33 +++++++++------- finance/escrow/kani-proofs/src/lib.rs | 26 +++++++------ finance/fundraiser/anchor-v1/README.md | 2 +- finance/fundraiser/anchor/README.md | 2 +- finance/fundraiser/kani-proofs/Cargo.toml | 2 +- finance/fundraiser/kani-proofs/README.md | 27 +++++++------ finance/fundraiser/kani-proofs/src/lib.rs | 12 ++++-- finance/lending/anchor-v1/README.md | 6 +-- .../programs/lending/src/constants.rs | 2 +- finance/lending/anchor/README.md | 6 +-- .../anchor/programs/lending/src/constants.rs | 2 +- finance/lending/kani-proofs/Cargo.toml | 4 +- finance/lending/kani-proofs/README.md | 35 +++++++++-------- finance/lending/kani-proofs/src/lib.rs | 12 ++++-- finance/lending/quasar/src/constants.rs | 2 +- finance/lending/quasar/src/math.rs | 2 +- finance/managed-fund/kani-proofs/Cargo.toml | 2 +- finance/managed-fund/kani-proofs/README.md | 23 ++++++----- finance/managed-fund/kani-proofs/src/lib.rs | 11 ++++-- finance/options/anchor-v1/README.md | 8 ++-- finance/options/anchor/README.md | 8 ++-- finance/options/kani-proofs/README.md | 23 ++++++----- finance/options/kani-proofs/src/lib.rs | 14 ++++--- finance/order-book/kani-proofs/Cargo.toml | 2 +- finance/order-book/kani-proofs/README.md | 32 +++++++++------- finance/order-book/kani-proofs/src/lib.rs | 13 ++++--- finance/perpetual-futures/anchor-v1/README.md | 4 +- finance/perpetual-futures/anchor/README.md | 4 +- .../quasar/src/instructions/shared.rs | 2 +- finance/prop-amm/kani-proofs/Cargo.toml | 2 +- finance/prop-amm/kani-proofs/README.md | 25 +++++++----- finance/prop-amm/kani-proofs/src/lib.rs | 20 ++++++---- finance/token-swap/anchor-v1/README.md | 2 +- finance/token-swap/anchor/README.md | 2 +- finance/token-swap/kani-proofs/Cargo.toml | 2 +- finance/token-swap/kani-proofs/README.md | 33 +++++++++------- finance/token-swap/kani-proofs/src/lib.rs | 38 +++++++++++-------- llms.txt | 4 +- .../quasar-metadata/src/instructions/mod.rs | 2 +- 46 files changed, 307 insertions(+), 226 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index b0b442932..39288e86c 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -1,27 +1,30 @@ name: Kani -# Formal-verification proofs (https://github.com/model-checking/kani) for the +# Kani model checks (https://github.com/model-checking/kani) for the # finance/ example programs. Each /kani-proofs crate models its -# program's pure money-math and lets the Kani model checker prove the invariants -# exhaustively, in the spirit of aeyakovenko/percolator. +# program's pure arithmetic and lets the Kani model checker check the invariants +# exhaustively over each harness's declared inputs, in the spirit of +# aeyakovenko/percolator. Kani marks a harness with #[kani::proof], which is why +# the crates are named kani-proofs and the harnesses proof_*; each one is a +# model check. # # WHY THIS RUNS ON A WEEKLY SCHEDULE, NOT ON EVERY PUSH/PR # ------------------------------------------------------- -# Most of the finance proofs verify NONLINEAR 128-bit arithmetic (constant- +# Most of the finance harnesses check NONLINEAR 128-bit arithmetic (constant- # product curves, mul_div with a symbolic divisor, integer sqrt, pari-mutuel # payouts, share exchange rates). Kani is a bit-precise model checker: it # bit-blasts that arithmetic into SAT, and nonlinear / symbolic-divisor terms # are the worst case for the solver. Even with bounded inputs, individual # harnesses take tens of seconds and a full crate runs for minutes; the whole # finance suite is far too slow to gate every push/PR. So the heavy -# `cargo kani` verification runs once a week (and on demand via +# `cargo kani` model check runs once a week (and on demand via # workflow_dispatch), while a fast unit-test job still runs on every push/PR to # catch model regressions early. See each finance//kani-proofs/README.md # for the per-harness bounds and timings. on: schedule: - # Mondays at 06:00 UTC. Weekly because the proofs are slow (see header). + # Mondays at 06:00 UTC. Weekly because the model checks are slow (see header). - cron: "0 6 * * 1" workflow_dispatch: {} # Fast feedback only: the unit-test job below is gated to these events; the @@ -43,9 +46,9 @@ env: FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true jobs: - # Fast feedback on every push/PR: the proof crates compile and their plain + # Fast feedback on every push/PR: the Kani crates compile and their plain # unit tests pass on stable, independently of the (slow) Kani toolchain. This - # catches model regressions without paying for full verification. + # catches model regressions without paying for the full model check. unit-tests: name: Proof unit tests (${{ matrix.program }}) runs-on: ubuntu-latest @@ -67,7 +70,7 @@ jobs: - uses: dtolnay/rust-toolchain@stable with: components: rustfmt, clippy - # Each proof crate declares its own `[workspace]`, so the repository-wide + # Each Kani crate declares its own `[workspace]`, so the repository-wide # `cargo fmt` and `cargo clippy` jobs in rust.yml never see it. Lint here # instead, or these crates drift. - name: Enforce formatting @@ -80,15 +83,15 @@ jobs: working-directory: finance/${{ matrix.program }}/kani-proofs run: cargo test - # The formal verification itself. SLOW (minutes per crate), so it only runs on - # the weekly schedule or when triggered manually — never on push/PR. The - # official Kani action installs the verifier + CBMC toolchain (with caching) - # and runs `cargo kani` in each proof crate; any failed proof fails the job. + # The model check itself. SLOW (minutes per crate), so it only runs on the + # weekly schedule or when triggered manually, never on push/PR. The official + # Kani action installs the model checker + CBMC toolchain (with caching) and + # runs `cargo kani` in each Kani crate; any failed harness fails the job. verify: name: Kani proofs (${{ matrix.program }}) if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest - # Every crate's proofs complete in under ~3 minutes. A harness whose bounds + # Every crate's harnesses complete in under ~3 minutes. A harness whose bounds # make the solver blow up otherwise runs into the runner's 6-hour hard # limit and surfaces as an easy-to-miss "cancelled" run (this happened: # prop-amm's quote-bracketing harness with an unbounded u64 price). Fail diff --git a/README.md b/README.md index f6dd5c39c..95bf831b9 100644 --- a/README.md +++ b/README.md @@ -32,7 +32,7 @@ To deploy to mainnet or devnet you'll need an RPC endpoint. [Quicknode](https:// ## Financial software ("DeFi") -The programs are examples of common financial primitives on Solana. As well as tests these all have [formal verification using Kani](https://github.com/model-checking/kani). Every finance program ships with proofs that verify its money-math invariants exhaustively over all inputs. See each program's `kani-proofs/` directory for the harnesses and what they prove. +The programs are examples of common financial primitives on Solana. As well as tests these all have [Kani](https://github.com/model-checking/kani) model checks. Every finance program ships with Kani harnesses that check its arithmetic invariants exhaustively over the inputs each harness declares. Kani marks a harness with `#[kani::proof]`, which is why each program's directory is `kani-proofs/` and the harnesses are named `proof_*`; each one is a model check. See each program's `kani-proofs/` directory for the harnesses and what they check. ### Escrow @@ -427,7 +427,7 @@ Work through the [finance examples](#financial-software-defi) in order of comple ### Are these examples production-ready? -They are teaching examples: every one builds and passes CI, and the finance programs additionally carry [Kani](https://github.com/model-checking/kani) formal-verification proofs of their money math. None are audited or deployed to mainnet, so treat them as reference implementations to learn from, not code to deploy as-is. +They are teaching examples: every one builds and passes CI, and the finance programs additionally carry [Kani](https://github.com/model-checking/kani) model checks of their arithmetic. None are audited or deployed to mainnet, so treat them as reference implementations to learn from, not code to deploy as-is. ## Acknowledgements diff --git a/finance/betting-market/kani-proofs/Cargo.toml b/finance/betting-market/kani-proofs/Cargo.toml index e3720fb3e..7521a7765 100644 --- a/finance/betting-market/kani-proofs/Cargo.toml +++ b/finance/betting-market/kani-proofs/Cargo.toml @@ -1,7 +1,7 @@ # Standalone workspace - intentionally NOT part of the root program-examples # workspace. Kani (https://github.com/model-checking/kani) proof harnesses that # model the betting market's pari-mutuel payout math (settlement fee/split and -# the pro-rata winner payout) so the model checker can verify solvency and +# the pro-rata winner payout) so the model checker can check solvency and # conservation without the Solana / SPL-token CPI machinery, which Kani cannot # symbolically execute. [workspace] diff --git a/finance/betting-market/kani-proofs/README.md b/finance/betting-market/kani-proofs/README.md index b872e1a17..87ad519c3 100644 --- a/finance/betting-market/kani-proofs/README.md +++ b/finance/betting-market/kani-proofs/README.md @@ -1,16 +1,20 @@ -# Betting-market: Kani proofs +# Betting-market: Kani model checks -Formal-verification harnesses for the pari-mutuel betting market, in the spirit +Kani harnesses that model-check the pari-mutuel betting market, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`, +which is why the crate is `kani-proofs` and the harnesses are named `proof_*`; +each one is a model check: Kani tries every value of the inputs the harness +declares and reports either that every assertion held or an input that breaks +one. -## What is verified +## What is checked Every stake lands in one vault; at settlement the losing pool (minus a fee) is split among the winners in proportion to their stake. The token movement goes through SPL CPIs Kani cannot symbolically execute, but the payout math is pure -integer arithmetic. This crate reproduces it faithfully and proves: +integer arithmetic. This crate reproduces it faithfully and checks, for every input: - `proof_settlement_fee_and_split`: `fee <= losing_pool` (so `distributable` never underflows) and `winning + distributable + fee == total`, settlement conserves the pool. - `proof_winner_never_below_stake`: `payout = stake + winnings >= stake`: a winner is never paid less than they staked (the fee is charged only on losers). @@ -19,7 +23,7 @@ integer arithmetic. This crate reproduces it faithfully and proves: - `proof_betting_and_settlement_windows_partition_time`: at every instant exactly one of `betting_is_open` and `may_settle` holds, so no bet can land once the event can be settled. - `proof_outcomes_fixed_before_money_arrives`: a model of the event's lifecycle guards (`add_outcome`, `open_betting`, `place_bet`, `settle_event`, `cancel_event`), run over every sequence of six calls at arbitrary times from a fresh draft. The outcome list never changes once money is in the pool, every stake lands in a market with at least two outcomes and before the close time, and settlement happens only at or after it. -### The solvency proof +### The solvency check After settlement the vault holds `winning_pool + distributable_losing_pool`. Each winner is paid `stake_i + floor(stake_i · D / winning_pool)`, and the @@ -31,11 +35,11 @@ the vault below zero; floor rounding only ever leaves dust behind. Modelled with ## Bounded model checking -The settlement, payout, and solvency proofs verify nonlinear 128-bit arithmetic +The settlement, payout, and solvency harnesses check nonlinear 128-bit arithmetic (`stake · distributable`, divided by the symbolic winning pool), the hard case for a bit-precise solver, so (as percolator does) they bound their symbolic inputs to a representative range; the pro-rata identity is scale-invariant. The -refund proof is pure linear logic and runs at full `u64` width (bounded only in +refund harness is pure linear logic and runs at full `u64` width (bounded only in the number of bettors). - `proof_settlement_fee_and_split`: `total_pool <= 4095`, `fee_bps` symbolic, ~1s @@ -45,12 +49,12 @@ the number of bettors). - `proof_betting_and_settlement_windows_partition_time`: full `i64`, <1s - `proof_outcomes_fixed_before_money_arrives`: 6 calls, full `u64` stakes and `i64` times, ~2s -Run weekly in CI (the `.github/workflows/kani.yml` `verify` job), not on every push/PR, because the bounded nonlinear proofs are slow. A fast unit-test job runs per push/PR. +Run weekly in CI (the `.github/workflows/kani.yml` `verify` job), not on every push/PR, because the bounded nonlinear model checks are slow. A fast unit-test job runs per push/PR. ## Running ```bash cargo test # unit tests, no Kani cargo install --locked kani-verifier && cargo kani setup # one-time -cargo kani # formal verification +cargo kani # Kani model checks ``` diff --git a/finance/betting-market/kani-proofs/src/lib.rs b/finance/betting-market/kani-proofs/src/lib.rs index 899118427..ac9fc288f 100644 --- a/finance/betting-market/kani-proofs/src/lib.rs +++ b/finance/betting-market/kani-proofs/src/lib.rs @@ -1,17 +1,20 @@ -//! Kani proof harnesses for the betting-market program (`finance/betting-market`). +//! Kani harnesses for the betting-market program (`finance/betting-market`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check the arithmetic of a DeFi engine's pure numeric core. Kani marks a +//! harness with `#[kani::proof]`, which is why the crate is `kani-proofs` and +//! the harnesses are named `proof_*`; each one is a model check over every value +//! of the inputs it declares. //! //! The program is a pari-mutuel betting market: every stake lands in one vault, //! and at settlement the losing pool (minus a fee) is split among the winners in //! proportion to their stake. The token movement goes through SPL CPIs Kani //! cannot symbolically execute, but the payout math (`settle_event`, //! `claim_winnings`) is pure integer arithmetic. This crate reproduces it -//! faithfully and proves the two properties that matter: **solvency** (winners +//! faithfully and checks the two properties that matter: **solvency** (winners //! can never collectively claim more than the vault holds) and that a winner is //! never paid less than their own stake. A small model of the event's -//! lifecycle guards also proves the outcome list is fixed before any money +//! lifecycle guards also checks that the outcome list is fixed before any money //! arrives and that the betting and settlement windows never overlap. //! //! The nonlinear harness uses bounded model checking (small symbolic inputs), as diff --git a/finance/escrow/anchor-v1/README.md b/finance/escrow/anchor-v1/README.md index 30744fd8b..05f4f54df 100644 --- a/finance/escrow/anchor-v1/README.md +++ b/finance/escrow/anchor-v1/README.md @@ -61,9 +61,9 @@ Yes. Escrow is the smallest complete finance program: one state PDA, one vault, Build with `anchor build`, then run `cargo test`. The tests are Rust integration tests against [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm), so no local validator is needed. -### How is this escrow program verified? +### How is this escrow program tested? -Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/) that check the money-math invariants over all possible inputs, not just test cases. +Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/) that check the arithmetic invariants for every input in their declared ranges, not just test cases. ## Credit diff --git a/finance/escrow/anchor/README.md b/finance/escrow/anchor/README.md index fa6118177..4954750c1 100644 --- a/finance/escrow/anchor/README.md +++ b/finance/escrow/anchor/README.md @@ -61,9 +61,9 @@ Yes. Escrow is the smallest complete finance program: one state PDA, one vault, Build with `anchor build`, then run `cargo test`. The tests are Rust integration tests against [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm), so no local validator is needed. -### How is this escrow program verified? +### How is this escrow program tested? -Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/) that check the money-math invariants over all possible inputs, not just test cases. +Two ways: LiteSVM integration tests covering the make, take, and cancel flows, and [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/) that check the arithmetic invariants for every input in their declared ranges, not just test cases. ## Credit diff --git a/finance/escrow/kani-proofs/README.md b/finance/escrow/kani-proofs/README.md index 40b7e63fb..8bf2ffdcc 100644 --- a/finance/escrow/kani-proofs/README.md +++ b/finance/escrow/kani-proofs/README.md @@ -1,18 +1,23 @@ -# Escrow: Kani proofs +# Escrow: Kani model checks -Formal-verification harnesses for the escrow program, in the spirit of +Kani model-check harnesses for the escrow program, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. -## What is verified +Kani marks a harness with `#[kani::proof]`, which is why the crate is +`kani-proofs` and the harnesses are named `proof_*`; each one is a model check: +it tries every value of its declared inputs and reports either that every +assertion held or the input that breaks one. + +## What is checked The escrow program itself does almost no arithmetic, it delegates token movement to the SPL token program through CPIs, which Kani cannot symbolically -execute. So (exactly like percolator, which verifies a self-contained library) -this crate models the escrow's *verifiable core* as pure Rust functions that -mirror the on-chain code's arithmetic and statement ordering, and proves the -invariants the program relies on: +execute. So (exactly like percolator, which model-checks a self-contained +library) this crate models the escrow's *checkable core* as pure Rust functions +that mirror the on-chain code's arithmetic and statement ordering, and checks +the invariants the program relies on: - `proof_token_transfer_conserves`: An SPL transfer either fails atomically or conserves the two accounts' total balance. - `proof_close_offer_conserves_on_success`: Closing the offer account conserves lamports and empties the source. @@ -54,16 +59,16 @@ let new_destination_lamports = destination_lamports **offer_info.lamports.borrow_mut() = 0; ``` -`proof_close_offer_conserves_lamports_unconditionally` now proves lamport +`proof_close_offer_conserves_lamports_unconditionally` now checks that lamport conservation holds with **equality on every path**, with no precondition, the invariant no longer depends on the runtime reverting a failed instruction. (This -is also why it's a plain proof, not a `#[kani::should_panic]`: a should-panic +is also why it's a plain harness, not a `#[kani::should_panic]`: a should-panic encoding would have *started failing* the moment this fix landed.) ## CI -These proofs run **weekly** (and on demand) in the `.github/workflows/kani.yml` -`verify` job, alongside the other `finance/` proof crates, the nonlinear ones +These model checks run **weekly** (and on demand) in the `.github/workflows/kani.yml` +`verify` job, alongside the other `finance/` Kani crates, the nonlinear ones are slow, so the full Kani run is scheduled rather than gating every push/PR. A fast `cargo test` job runs per push/PR to catch model regressions early. @@ -73,7 +78,7 @@ fast `cargo test` job runs per push/PR to catch model regressions early. # Plain unit tests (no Kani required): cargo test -# Formal verification (requires Kani): +# Kani model checks (requires Kani): cargo install --locked kani-verifier && cargo kani setup # one-time cargo kani ``` diff --git a/finance/escrow/kani-proofs/src/lib.rs b/finance/escrow/kani-proofs/src/lib.rs index d9c621a2d..e00dd605a 100644 --- a/finance/escrow/kani-proofs/src/lib.rs +++ b/finance/escrow/kani-proofs/src/lib.rs @@ -1,21 +1,25 @@ -//! Kani proof harnesses for the Solana escrow program. +//! Kani model-check harnesses for the Solana escrow program. //! -//! Inspired by aeyakovenko/percolator, which uses Kani to prove the -//! mathematical correctness of a risk engine's pure computational core. +//! Inspired by aeyakovenko/percolator, which uses Kani to check the +//! arithmetic of a risk engine's pure computational core. //! //! Kani is a bit-precise model checker: a `#[kani::proof]` harness explores //! *every* possible value of its `kani::any()` inputs and reports any input //! for which an `assert!` can fail (or for which arithmetic overflows, etc.). +//! That is a model check, not a formal proof. Kani marks a harness with +//! `#[kani::proof]`, which is why the crate is `kani-proofs` and the harnesses +//! are named `proof_*`; each one is a model check. //! -//! ## Why model instead of verifying the program crate directly +//! ## Why model instead of checking the program crate directly //! //! The escrow program does almost no arithmetic itself: it hands the actual //! token movement to the SPL token program through cross-program invocations //! (`invoke` / `invoke_signed`). Those CPIs are opaque syscalls that Kani //! cannot symbolically execute, and the program types (`AccountInfo`, `Pubkey`, //! borsh buffers) are awkward to make symbolic. So — exactly like percolator, -//! which verifies a self-contained library — we model the escrow's verifiable -//! core as pure functions and prove the invariants the on-chain code relies on: +//! which model-checks a self-contained library — we model the escrow's +//! checkable core as pure functions and check the invariants the on-chain code +//! relies on: //! //! 1. `token_transfer` - faithful model of an SPL `transfer_checked`. //! 2. lamport closing - models `utils::close_offer_account`. @@ -23,7 +27,7 @@ //! 4. seed round-trip - the `id.to_le_bytes()` PDA seed math. //! //! Each model mirrors the real code's arithmetic and statement ordering so the -//! proofs say something meaningful about the deployed program. +//! model checks say something meaningful about the deployed program. #![cfg_attr(kani, allow(dead_code))] @@ -102,7 +106,7 @@ fn proof_token_transfer_conserves() { // // This model preserves that ordering. Because the credit is computed before any // account is touched, the error path mutates nothing, so lamport conservation -// holds with EQUALITY on every path (see proof below) — not merely "no inflation". +// holds with EQUALITY on every path (see harness below) — not merely "no inflation". /// Lamport-overflow error, mirroring `EscrowError::ArithmeticOverflow`. #[derive(Debug, PartialEq, Eq)] @@ -150,7 +154,7 @@ fn proof_close_offer_conserves_on_success() { /// meant conservation held only because of those *external* guarantees. The /// function now computes the credited balance before touching any account /// (`native/.../utils.rs`), so the error path mutates nothing and conservation -/// holds with equality regardless of the result. This proof asserts exactly +/// holds with equality regardless of the result. This harness asserts exactly /// that, with no precondition on the inputs. #[cfg(kani)] #[kani::proof] @@ -268,7 +272,7 @@ fn proof_take_offer_conserves_value() { /// and `maker_b_before + wanted_b` fit in `u64` — otherwise the transfer would /// have failed first. So `.ok_or(ArithmeticOverflow)` and the subsequent /// `TokenConservationViolation` comparison are belt-and-suspenders checks that -/// cannot fire. Kani proves this directly, without needing to assume any +/// cannot fire. Kani checks this directly, without needing to assume any /// external SPL invariant (the model already encodes it). #[cfg(kani)] #[kani::proof] @@ -294,7 +298,7 @@ fn proof_take_offer_guard_never_overflows() { /// Companion to the finding above: once we assume the SPL invariant that a /// receiver's post-balance fits in `u64` (which is exactly the precondition /// under which the `transfer_checked` calls succeed), the `ConservationOverflow` -/// arm is provably unreachable. This proof PASSES, confirming the guard is dead +/// arm is unreachable for every input. This harness PASSES, confirming the guard is dead /// code rather than a real bug. #[cfg(kani)] #[kani::proof] diff --git a/finance/fundraiser/anchor-v1/README.md b/finance/fundraiser/anchor-v1/README.md index 77a19f769..971a4d619 100644 --- a/finance/fundraiser/anchor-v1/README.md +++ b/finance/fundraiser/anchor-v1/README.md @@ -176,4 +176,4 @@ Contributors call `refund` after the deadline to reclaim exactly what they put i ### How is this fundraiser tested and verified? -`anchor build` then `cargo test` runs LiteSVM tests that warp the clock across the deadline to exercise contribution windows, per-contributor caps, claims, refunds, and closing. The money math has [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/). +`anchor build` then `cargo test` runs LiteSVM tests that warp the clock across the deadline to exercise contribution windows, per-contributor caps, claims, refunds, and closing. The arithmetic has [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/). diff --git a/finance/fundraiser/anchor/README.md b/finance/fundraiser/anchor/README.md index 439023ed0..31b463231 100644 --- a/finance/fundraiser/anchor/README.md +++ b/finance/fundraiser/anchor/README.md @@ -177,4 +177,4 @@ Contributors call `refund` after the deadline to reclaim exactly what they put i ### How is this fundraiser tested and verified? -`anchor build` then `cargo test` runs LiteSVM tests that warp the clock across the deadline to exercise contribution windows, per-contributor caps, claims, refunds, and closing. The money math has [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/). +`anchor build` then `cargo test` runs LiteSVM tests that warp the clock across the deadline to exercise contribution windows, per-contributor caps, claims, refunds, and closing. The arithmetic has [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/). diff --git a/finance/fundraiser/kani-proofs/Cargo.toml b/finance/fundraiser/kani-proofs/Cargo.toml index 397035e94..c9b5828e1 100644 --- a/finance/fundraiser/kani-proofs/Cargo.toml +++ b/finance/fundraiser/kani-proofs/Cargo.toml @@ -1,6 +1,6 @@ # Standalone workspace - intentionally NOT part of the root program-examples # workspace. Kani (https://github.com/model-checking/kani) proof harnesses -# modelling this program's pure money-math so the model checker can verify the +# modelling this program's pure arithmetic so the model checker can check the # invariants without the Solana / SPL-token CPI machinery, which Kani cannot # symbolically execute. [workspace] diff --git a/finance/fundraiser/kani-proofs/README.md b/finance/fundraiser/kani-proofs/README.md index 57de49755..dd4ebba7e 100644 --- a/finance/fundraiser/kani-proofs/README.md +++ b/finance/fundraiser/kani-proofs/README.md @@ -1,33 +1,38 @@ -# Fundraiser: Kani proofs +# Fundraiser: Kani model checks -Formal-verification harnesses for the fundraiser program, in the spirit of +Kani harnesses for the fundraiser program, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`, +which is why the crate is `kani-proofs` and the harnesses are named `proof_*`; +each one is a model check: Kani tries every value of the inputs the harness +declares and reports either that every assertion held or the input that breaks +one. -## What is verified +## What is checked The program collects contributions toward a goal; if the goal is not met by the deadline, every contributor reclaims their exact stake. Token movement is via SPL CPIs Kani cannot symbolically execute, but the accounting (`contribute`, -`refund`) is pure integer arithmetic: +`refund`) is pure integer arithmetic, and the harnesses check it for every input in the +declared ranges: - `proof_contribution_cap_bounds`: The per-contributor cap never exceeds the goal, and the `cumulative <= cap` check keeps every contributor at or below it (and below the goal). - `proof_current_amount_is_sum_of_contributions`: `current_amount` always equals the sum of the contributions added to it, no accounting drift. - `proof_refunds_sum_to_current_amount`: On a failed raise, refunds sum back to `current_amount`; no contributor reclaims more than they put in. -The cap proof verifies nonlinear arithmetic (`goal · pct / scaler`) and uses -bounded model checking; the two accounting/refund proofs are pure linear logic +The cap harness checks nonlinear arithmetic (`goal · pct / scaler`) over +bounded inputs; the two accounting/refund harnesses are pure linear logic and run at full `u64` width (bounded only in the number of contributors). The -whole suite verifies in under a second. +whole suite finishes in under a second. Run weekly in CI (the `kani.yml` `verify` job), not on every push/PR, because -the nonlinear proofs are slow. A fast unit-test job runs per push/PR. +the nonlinear model checks are slow. A fast unit-test job runs per push/PR. ## Running ```bash cargo test # unit tests, no Kani cargo install --locked kani-verifier && cargo kani setup # one-time -cargo kani # formal verification +cargo kani # model check ``` diff --git a/finance/fundraiser/kani-proofs/src/lib.rs b/finance/fundraiser/kani-proofs/src/lib.rs index 7fbb5f5af..be1f9e2d5 100644 --- a/finance/fundraiser/kani-proofs/src/lib.rs +++ b/finance/fundraiser/kani-proofs/src/lib.rs @@ -1,19 +1,23 @@ -//! Kani proof harnesses for the fundraiser program (`finance/fundraiser`). +//! Kani harnesses for the fundraiser program (`finance/fundraiser`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check a DeFi engine's pure numeric core. Kani marks a harness with +//! `#[kani::proof]`, which is why the crate is `kani-proofs` and the harnesses +//! are named `proof_*`; each one is a model check: Kani tries every value of +//! the inputs the harness declares and reports either that every assertion +//! held or the input that breaks one. //! //! The program collects contributions into a vault toward a goal; if the goal //! is not met by the deadline, every contributor reclaims their exact stake. //! Token movement is via SPL CPIs Kani cannot symbolically execute, but the //! accounting (`contribute`, `refund`) is pure integer arithmetic. This crate -//! reproduces it faithfully and proves the per-contributor cap, the running- +//! reproduces it faithfully and checks the per-contributor cap, the running- //! total accounting, and refund conservation. #![cfg_attr(kani, allow(dead_code))] /// `contribute::MAX_CONTRIBUTION_PERCENTAGE` / `PERCENTAGE_SCALER`. The program -/// ships these as a percentage cap; the exact values do not matter to the proof, +/// ships these as a percentage cap; the exact values do not matter to the check, /// only that the cap is `goal * pct / scaler`. pub const MAX_CONTRIBUTION_PERCENTAGE: u128 = 10; // 10% pub const PERCENTAGE_SCALER: u128 = 100; diff --git a/finance/lending/anchor-v1/README.md b/finance/lending/anchor-v1/README.md index 05a61901b..2bec03221 100644 --- a/finance/lending/anchor-v1/README.md +++ b/finance/lending/anchor-v1/README.md @@ -135,7 +135,7 @@ less, which would make the liquidator overpay. ### Fixed-point math -All money math is integer-only `u128`: no floats, no fixed-point crates. Ratios +All arithmetic is integer-only `u128`: no floats, no fixed-point crates. Ratios (rates, the index, the exchange rate, obligation values) are scaled by `FIXED_POINT_SCALE` (10^18). Every conversion rounds in the protocol's favour (user output floored, debt ceiled), so dust cannot be extracted by repeated @@ -230,6 +230,6 @@ Through a cumulative accumulation factor: `refresh_reserve` advances a per-reser The admin `set_price` instruction handler stands in for an oracle feed in this example. `refresh_obligation` re-values collateral and debt at those prices before any borrow, withdraw, or liquidation is allowed, and stale reserves or prices are rejected. -### How is this lending program tested and verified? +### How is this lending program tested? -`anchor build` then `cargo test` runs LiteSVM integration tests covering interest accrual, borrowing at the LTV limit, liquidation after a price move, and the share-inflation guard. The money math also has [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/). +`anchor build` then `cargo test` runs LiteSVM integration tests covering interest accrual, borrowing at the LTV limit, liquidation after a price move, and the share-inflation guard. The arithmetic also has [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/). diff --git a/finance/lending/anchor-v1/programs/lending/src/constants.rs b/finance/lending/anchor-v1/programs/lending/src/constants.rs index 125e5356f..8eb01c965 100644 --- a/finance/lending/anchor-v1/programs/lending/src/constants.rs +++ b/finance/lending/anchor-v1/programs/lending/src/constants.rs @@ -7,7 +7,7 @@ /// cumulative borrow-rate index, the share-token exchange rate, and obligation /// values. A ratio `r` is stored as the integer `r * FIXED_POINT_SCALE`. /// -/// All money math is integer-only (no floats, no fixed-point crates). 10^18 +/// All arithmetic is integer-only (no floats, no fixed-point crates). 10^18 /// keeps a single second's interest, which can be a tiny fraction of the index, /// from truncating to zero, while u128's ~3.4e38 ceiling leaves headroom for the /// index to grow and for intermediate products before the final narrowing cast. diff --git a/finance/lending/anchor/README.md b/finance/lending/anchor/README.md index b076bd9c0..f097a89f7 100644 --- a/finance/lending/anchor/README.md +++ b/finance/lending/anchor/README.md @@ -135,7 +135,7 @@ less, which would make the liquidator overpay. ### Fixed-point math -All money math is integer-only `u128`: no floats, no fixed-point crates. Ratios +All arithmetic is integer-only `u128`: no floats, no fixed-point crates. Ratios (rates, the index, the exchange rate, obligation values) are scaled by `FIXED_POINT_SCALE` (10^18). Every conversion rounds in the protocol's favour (user output floored, debt ceiled), so dust cannot be extracted by repeated @@ -230,6 +230,6 @@ Through a cumulative accumulation factor: `refresh_reserve` advances a per-reser The admin `set_price` instruction handler stands in for an oracle feed in this example. `refresh_obligation` re-values collateral and debt at those prices before any borrow, withdraw, or liquidation is allowed, and stale reserves or prices are rejected. -### How is this lending program tested and verified? +### How is this lending program tested? -`anchor build` then `cargo test` runs LiteSVM integration tests covering interest accrual, borrowing at the LTV limit, liquidation after a price move, and the share-inflation guard. The money math also has [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/). +`anchor build` then `cargo test` runs LiteSVM integration tests covering interest accrual, borrowing at the LTV limit, liquidation after a price move, and the share-inflation guard. The arithmetic also has [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/). diff --git a/finance/lending/anchor/programs/lending/src/constants.rs b/finance/lending/anchor/programs/lending/src/constants.rs index 125e5356f..8eb01c965 100644 --- a/finance/lending/anchor/programs/lending/src/constants.rs +++ b/finance/lending/anchor/programs/lending/src/constants.rs @@ -7,7 +7,7 @@ /// cumulative borrow-rate index, the share-token exchange rate, and obligation /// values. A ratio `r` is stored as the integer `r * FIXED_POINT_SCALE`. /// -/// All money math is integer-only (no floats, no fixed-point crates). 10^18 +/// All arithmetic is integer-only (no floats, no fixed-point crates). 10^18 /// keeps a single second's interest, which can be a tiny fraction of the index, /// from truncating to zero, while u128's ~3.4e38 ceiling leaves headroom for the /// index to grow and for intermediate products before the final narrowing cast. diff --git a/finance/lending/kani-proofs/Cargo.toml b/finance/lending/kani-proofs/Cargo.toml index e2351f371..ed116d130 100644 --- a/finance/lending/kani-proofs/Cargo.toml +++ b/finance/lending/kani-proofs/Cargo.toml @@ -1,8 +1,8 @@ # Standalone workspace - intentionally NOT part of the root program-examples # workspace. Kani (https://github.com/model-checking/kani) proof harnesses that -# model the lending program's pure money-math (mul_div floor/ceil with +# model the lending program's pure arithmetic (mul_div floor/ceil with # directional rounding, the kinked interest-rate curve, index compounding, the -# share exchange rate, and liquidation sizing) so the model checker can verify +# share exchange rate, and liquidation sizing) so the model checker can check # the invariants without the Solana / SPL-token CPI machinery, which Kani # cannot symbolically execute. [workspace] diff --git a/finance/lending/kani-proofs/README.md b/finance/lending/kani-proofs/README.md index 0aaacafc1..eac2d2af6 100644 --- a/finance/lending/kani-proofs/README.md +++ b/finance/lending/kani-proofs/README.md @@ -1,22 +1,27 @@ -# Lending: Kani proofs +# Lending: Kani model checks -Formal-verification harnesses for the lending program, in the spirit of +Kani model-check harnesses for the lending program, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. + +Kani marks a harness with `#[kani::proof]`, which is why the crate is +`kani-proofs` and the harnesses are named `proof_*`; each one is a model check: +it tries every value of its declared inputs and reports either that every +assertion held or the input that breaks one. This is the richest of the finance examples (a Solend-style pool) so it gets -the most proofs. +the most harnesses. -## What is verified +## What is checked The token movement is delegated to SPL CPIs Kani cannot symbolically execute, -but the money-math is pure integer arithmetic. This crate reproduces the -formulas faithfully and proves their invariants: +but everything else is pure integer arithmetic. This crate reproduces the +formulas faithfully and checks their invariants: - `proof_mul_div_floor_ceil_correct`: `mul_div_floor`/`mul_div_ceil` are the true floor/ceil of `a·b/d`, differ by ≤ 1, and coincide iff the division is exact. - `proof_rounding_is_protocol_favourable`: `ceil ≥ floor` always, debt (rounded up) is never undercounted and a supplier claim (rounded down) never overcounted, so dust can't be extracted by round-trips. -- `proof_interest_index_monotonic`: The cumulative borrow-rate index never decreases (`accrue_interest` multiplies by a factor ≥ 1), borrowers always owe ≥ principal. +- `proof_accumulation_factor_monotonic`: The borrow accumulation factor never decreases (`accrue_interest` multiplies by a factor ≥ 1), borrowers always owe ≥ principal. - `proof_utilization_in_range`: Utilization is always a valid `[0, 10000]` bps fraction (`borrowed ≤ gross`). - `proof_borrow_rate_within_bounds`: The kinked rate curve stays within `[min_rate, max_rate]` for every utilization, given the config ordering `min ≤ optimal ≤ max`. - `proof_deposit_redeem_cannot_extract`: A deposit→redeem round-trip never returns more liquidity than was put in (both legs floor), no rounding drain of the pool. @@ -25,7 +30,7 @@ formulas faithfully and proves their invariants: ## Bounded model checking -All these harnesses verify **nonlinear 128-bit arithmetic**, and several divide +All these harnesses check **nonlinear 128-bit arithmetic**, and several divide by a *symbolic* divisor (`mul_div`'s `d`, the index `scale`, the rate curve's `full − optimal`), the single most expensive shape for a bit-precise solver. Following percolator's practice, each bounds its symbolic inputs to a @@ -33,7 +38,7 @@ representative range; the identities are scale-invariant, so every rounding / crossing boundary is still exercised. Two harnesses go further and make a normally-constant denominator a **parameter** -so the proof can use a small one: +so the harness can use a small one: - the accumulation factor uses a small symbolic `scale` instead of the real `FIXED_POINT_SCALE = 10^18` (the monotonicity property is scale-invariant); @@ -43,15 +48,15 @@ so the proof can use a small one: - `proof_mul_div_floor_ceil_correct`: `a, b, d <= 31`, ~37s - `proof_rounding_is_protocol_favourable`: `a, b, d <= 127`, ~29s -- `proof_interest_index_monotonic`: `old/accrued <= 255`, `scale <= 127`, ~5s +- `proof_accumulation_factor_monotonic`: `old/accrued <= 255`, `scale <= 127`, ~5s - `proof_utilization_in_range`: `<= 4095`, ~1s - `proof_borrow_rate_within_bounds`: rates `<= 255`, `full_utilization <= 32`, ~25s - `proof_deposit_redeem_cannot_extract`: `<= 31`, ~6s - `proof_liquidation_repay_bounded_by_debt`: `debt <= 4095`, <1s - `proof_seize_value_includes_bonus`: `repay_value <= 4095`, <1s -These proofs run **weekly in CI** (the `kani.yml` `verify` job), not on every -push/PR, because they are slow. A fast unit-test job runs per push/PR. +These model checks run **weekly in CI** (the `kani.yml` `verify` job), not on +every push/PR, because they are slow. A fast unit-test job runs per push/PR. ## Running @@ -59,7 +64,7 @@ push/PR, because they are slow. A fast unit-test job runs per push/PR. # Plain unit tests (no Kani required): cargo test -# Formal verification (requires Kani): +# Kani model checks (requires Kani): cargo install --locked kani-verifier && cargo kani setup # one-time cargo kani ``` diff --git a/finance/lending/kani-proofs/src/lib.rs b/finance/lending/kani-proofs/src/lib.rs index 41e4d67d5..1f594469c 100644 --- a/finance/lending/kani-proofs/src/lib.rs +++ b/finance/lending/kani-proofs/src/lib.rs @@ -1,7 +1,11 @@ -//! Kani proof harnesses for the lending program (`finance/lending`). +//! Kani model-check harnesses for the lending program (`finance/lending`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check the arithmetic of a DeFi engine's pure numeric core. +//! +//! Kani marks a harness with `#[kani::proof]`, which is why the crate is +//! `kani-proofs` and the harnesses are named `proof_*`; each one is a model +//! check, which tries every value of its declared inputs, not a formal proof. //! //! The lending program is the richest of the finance examples: a Solend-style //! pool with `mul_div` floor/ceil rounding (`math.rs`), a kinked interest-rate @@ -10,7 +14,7 @@ //! factor and bonus (`liquidate_obligation`). All of that is pure integer //! arithmetic; the token movement is delegated to SPL CPIs that Kani cannot //! symbolically execute. This crate reproduces the formulas faithfully and -//! proves the invariants the protocol's safety rests on. +//! checks the invariants the protocol's safety rests on. //! //! Nonlinear 128-bit arithmetic is the hard case for a bit-precise solver, so — //! as percolator does — the harnesses use bounded model checking: symbolic @@ -169,7 +173,7 @@ fn proof_utilization_in_range() { /// /// `full_utilization` is the 100%-utilization denominator — `BPS_DENOMINATOR` /// (10_000) on-chain. It is a parameter here only so the scale-invariant -/// in-bounds proof can use a small denominator: dividing by a symbolic value +/// in-bounds harness can use a small denominator: dividing by a symbolic value /// near 10_000 is intractable for the bit-precise solver, but the property is /// identical at any scale. pub fn borrow_rate_bps( diff --git a/finance/lending/quasar/src/constants.rs b/finance/lending/quasar/src/constants.rs index d2f86bd49..f6d691760 100644 --- a/finance/lending/quasar/src/constants.rs +++ b/finance/lending/quasar/src/constants.rs @@ -2,7 +2,7 @@ /// Fixed-point scale (10^18) for every ratio: interest rates, the cumulative /// borrow-rate index, the share-token exchange rate, and obligation values. -/// All money math is integer-only `u128`; a ratio `r` is stored as +/// All arithmetic is integer-only `u128`; a ratio `r` is stored as /// `r * FIXED_POINT_SCALE`. pub const FIXED_POINT_SCALE: u128 = 1_000_000_000_000_000_000; diff --git a/finance/lending/quasar/src/math.rs b/finance/lending/quasar/src/math.rs index cd8550dc5..0425ea8b3 100644 --- a/finance/lending/quasar/src/math.rs +++ b/finance/lending/quasar/src/math.rs @@ -1,4 +1,4 @@ -//! Integer-only money math (no floats, no fixed-point crates), shared by the +//! Integer-only arithmetic (no floats, no fixed-point crates), shared by the //! handlers. Ratios are scaled by `FIXED_POINT_SCALE`; conversions round in the //! protocol's favour. diff --git a/finance/managed-fund/kani-proofs/Cargo.toml b/finance/managed-fund/kani-proofs/Cargo.toml index 27642335c..8c6a795b2 100644 --- a/finance/managed-fund/kani-proofs/Cargo.toml +++ b/finance/managed-fund/kani-proofs/Cargo.toml @@ -1,6 +1,6 @@ # Standalone workspace - intentionally NOT part of the root program-examples # workspace. Kani (https://github.com/model-checking/kani) proof harnesses -# modelling this program's pure money-math so the model checker can verify the +# modelling this program's pure arithmetic so the model checker can check the # invariants without the Solana / SPL-token CPI machinery, which Kani cannot # symbolically execute. [workspace] diff --git a/finance/managed-fund/kani-proofs/README.md b/finance/managed-fund/kani-proofs/README.md index 13733f0dd..69f402a67 100644 --- a/finance/managed-fund/kani-proofs/README.md +++ b/finance/managed-fund/kani-proofs/README.md @@ -1,16 +1,21 @@ -# Managed-fund: Kani proofs +# Managed-fund: Kani model checks -Formal-verification harnesses for the ERC4626-style share vault, in the spirit +Kani harnesses that model-check the ERC4626-style share vault, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`, +which is why the crate is `kani-proofs` and the harnesses are named `proof_*`; +each one is a model check: Kani tries every value of the inputs the harness +declares and reports either that every assertion held or an input that breaks +one. -## What is verified +## What is checked Depositors mint share tokens against the fund's net asset value; withdrawals burn shares for a proportional slice of every vault balance; a manager fee mints a small slice of shares over time. Token movement is via SPL CPIs Kani cannot -symbolically execute, but the share math is pure integer arithmetic: +symbolically execute, but the share math is pure integer arithmetic. For every +input, the harnesses check: - `proof_withdraw_within_balance`: **Solvency**: a withdrawal never takes more of any vault balance than it holds (`floor(balance·shares/total) <= balance`, since `shares <= total`); burning the whole supply takes exactly the whole balance. - `proof_deposit_withdraw_cannot_extract`: A deposit→withdraw round-trip never returns more than was deposited, no rounding attack mints shares worth more than they cost. @@ -20,7 +25,7 @@ symbolically execute, but the share math is pure integer arithmetic: ## Bounded model checking -The nonlinear harnesses verify 128-bit arithmetic with a symbolic divisor (the share +The nonlinear harnesses check 128-bit arithmetic with a symbolic divisor (the share supply / NAV), so (as percolator does) they bound their symbolic inputs to a representative range; the share identities are scale-invariant. @@ -31,12 +36,12 @@ representative range; the share identities are scale-invariant. - `proof_fee_shares_bounded_by_supply`: `<= 255`, runs in ~4s Run weekly in CI (the `kani.yml` `verify` job), not on every push/PR, because -the bounded nonlinear proofs are slow. A fast unit-test job runs per push/PR. +the bounded nonlinear model checks are slow. A fast unit-test job runs per push/PR. ## Running ```bash cargo test # unit tests, no Kani cargo install --locked kani-verifier && cargo kani setup # one-time -cargo kani # formal verification +cargo kani # Kani model checks ``` diff --git a/finance/managed-fund/kani-proofs/src/lib.rs b/finance/managed-fund/kani-proofs/src/lib.rs index 0d6a8611e..64631e986 100644 --- a/finance/managed-fund/kani-proofs/src/lib.rs +++ b/finance/managed-fund/kani-proofs/src/lib.rs @@ -1,20 +1,23 @@ -//! Kani proof harnesses for the managed-fund program (`finance/managed-fund`). +//! Kani harnesses for the managed-fund program (`finance/managed-fund`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check the arithmetic of a DeFi engine's pure numeric core. Kani marks a +//! harness with `#[kani::proof]`, which is why the crate is `kani-proofs` and +//! the harnesses are named `proof_*`; each one is a model check over every value +//! of the inputs it declares. //! //! The program is an ERC4626-style share vault: depositors mint share tokens //! against the fund's net asset value, and withdrawals burn shares for a //! proportional slice of every vault balance. A manager fee mints a small slice //! of shares over time. Token movement is via SPL CPIs Kani cannot symbolically //! execute, but the share math (`deposit`, `withdraw`, `collect_fees`) is pure -//! integer arithmetic. This crate reproduces it faithfully and proves the +//! integer arithmetic. This crate reproduces it faithfully and checks the //! invariants the fund's solvency rests on. //! //! The program prices shares and pays withdrawals from the holdings it has //! recorded (`Fund::usdc_holdings` and `asset_holdings`), never from the //! vaults' token balances, so tokens donated straight into a vault are outside -//! the fund. The harnesses model a vault as a (recorded, balance) pair and prove +//! the fund. The harnesses model a vault as a (recorded, balance) pair and check //! what that buys: payouts never exceed the real balance, and a donation cannot //! dilute the next depositor. //! diff --git a/finance/options/anchor-v1/README.md b/finance/options/anchor-v1/README.md index ab89a7d18..1a0a28430 100644 --- a/finance/options/anchor-v1/README.md +++ b/finance/options/anchor-v1/README.md @@ -18,7 +18,7 @@ there is no margin, no liquidator, and no oracle. The venue that took the other road on Solana, cash settlement with margin and an oracle, is Zeta Markets. -[⚓ Anchor v2](../anchor) · [⚓ Anchor v1](.) · [💫 Quasar](../quasar) · [Kani proofs](../kani-proofs) +[⚓ Anchor v2](../anchor) · [⚓ Anchor v1](.) · [💫 Quasar](../quasar) · [Kani model checks](../kani-proofs) ## Programs @@ -170,8 +170,8 @@ holders' deliveries awaiting collection), `quote_locked` (put collateral, plus call holders' strike payments awaiting collection) and `fees_owed`. Every handler that moves tokens updates the ledger before any transfer and then asserts that each vault still covers what it owes (`CustodyInvariantViolated` -otherwise). The [Kani proofs](../kani-proofs) walk every path through an option's -life and show the ledger returns to zero. +otherwise). The [Kani model checks](../kani-proofs) walk every path through an option's +life and check that the ledger returns to zero. ## Design notes and further reading @@ -212,7 +212,7 @@ cargo test The LiteSVM suite (`programs/options/tests/test_options.rs`) walks the call from write to collected strike and the put from write to exercise and to expiry, pins every balance to the minor unit, checks the custody ledger -against the vault balances after every step, and proves every gate shuts: +against the vault balances after every step, and checks that every refusal holds: the expiry boundary from both sides, cancel after sale, buy after sale or expiry, exercise by a non-holder, collection by a non-writer or before exercise, reclaim after exercise, fee collection by a non-admin, and the diff --git a/finance/options/anchor/README.md b/finance/options/anchor/README.md index b333c7f98..d018618bc 100644 --- a/finance/options/anchor/README.md +++ b/finance/options/anchor/README.md @@ -18,7 +18,7 @@ there is no margin, no liquidator, and no oracle. The venue that took the other road on Solana, cash settlement with margin and an oracle, is Zeta Markets. -[⚓ Anchor v2](.) · [⚓ Anchor v1](../anchor-v1) · [💫 Quasar](../quasar) · [Kani proofs](../kani-proofs) +[⚓ Anchor v2](.) · [⚓ Anchor v1](../anchor-v1) · [💫 Quasar](../quasar) · [Kani model checks](../kani-proofs) ## Programs @@ -170,8 +170,8 @@ holders' deliveries awaiting collection), `quote_locked` (put collateral, plus call holders' strike payments awaiting collection) and `fees_owed`. Every handler that moves tokens updates the ledger before any transfer and then asserts that each vault still covers what it owes (`CustodyInvariantViolated` -otherwise). The [Kani proofs](../kani-proofs) walk every path through an option's -life and show the ledger returns to zero. +otherwise). The [Kani model checks](../kani-proofs) walk every path through an option's +life and check that the ledger returns to zero. ## Design notes and further reading @@ -212,7 +212,7 @@ cargo test The LiteSVM suite (`programs/options/tests/test_options.rs`) walks the call from write to collected strike and the put from write to exercise and to expiry, pins every balance to the minor unit, checks the custody ledger -against the vault balances after every step, and proves every gate shuts: +against the vault balances after every step, and checks that every refusal holds: the expiry boundary from both sides, cancel after sale, buy after sale or expiry, exercise by a non-holder, collection by a non-writer or before exercise, reclaim after exercise, fee collection by a non-admin, and the diff --git a/finance/options/kani-proofs/README.md b/finance/options/kani-proofs/README.md index 78a539c02..ea6dd8ccc 100644 --- a/finance/options/kani-proofs/README.md +++ b/finance/options/kani-proofs/README.md @@ -1,11 +1,15 @@ -# Options: Kani proofs +# Options: Kani model checks -Formal-verification harnesses for the fully collateralized options venue, in -the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), -which uses the [Kani](https://github.com/model-checking/kani) model checker to -prove the mathematical correctness of a DeFi engine. +Kani harnesses for the fully collateralized options venue, in the spirit of +[`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`, +which is why the crate is `kani-proofs` and the harnesses are named `proof_*`; +each one is a model check: Kani tries every value of the inputs the harness +declares and reports either that every assertion held or the input that breaks +one. -## What is verified +## What is checked The onchain instructions hand token movement to the SPL token program through CPIs that Kani cannot symbolically execute, but the arithmetic they rely on is @@ -14,7 +18,8 @@ integers the writer chose, the only rounding in the program is the floor in the fee split, and the expiry window is one comparison and its complement. This crate reproduces those formulas (mirroring `options::contract_math`) and the handlers' custody accounting (mirroring the `underlying_locked`, -`quote_locked` and `fees_owed` counters on the `Market` account) and proves: +`quote_locked` and `fees_owed` counters on the `Market` account) and checks, for every input +in the declared ranges: - `proof_exercise_moves_exactly_the_posted_terms`: for every option the program would accept, physical settlement hands the holder exactly the collateral @@ -49,7 +54,7 @@ argued to be independent of the bound: product overflows, so the overflow refusal is pinned by a unit test. - `proof_premium_split_conserves_the_premium`: premium and fee rate each at most `0xFF`. The split is a 128-bit multiply followed by a 128-bit division, - and proving a divider exact against a multiplier is the hardest shape of + and checking a divider exact against a multiplier is the hardest shape of problem a SAT solver sees: a 16-bit premium against the full fee range runs for hours. Eight bits on each side finish in about a second, exercise the floor on both sides of every carry, and the fee-equals-premium edge at the @@ -68,6 +73,6 @@ argued to be independent of the bound: # LiteSVM tests and the book chapter use: cargo test -# Full verification (requires cargo-kani): +# Full model check (requires cargo-kani): cargo kani ``` diff --git a/finance/options/kani-proofs/src/lib.rs b/finance/options/kani-proofs/src/lib.rs index d98f59ef3..d478bb512 100644 --- a/finance/options/kani-proofs/src/lib.rs +++ b/finance/options/kani-proofs/src/lib.rs @@ -1,14 +1,18 @@ -//! Kani proof harnesses for the options venue (`finance/options`). +//! Kani harnesses for the options venue (`finance/options`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check a DeFi engine's pure numeric core. Kani marks a harness with +//! `#[kani::proof]`, which is why the crate is `kani-proofs` and the harnesses +//! are named `proof_*`; each one is a model check: Kani tries every value of +//! the inputs the harness declares and reports either that every assertion +//! held or the input that breaks one. //! //! The on-chain instructions hand the actual token movement to the SPL token //! program via CPIs that Kani cannot symbolically execute. The arithmetic //! underneath is small and is reproduced here faithfully, mirroring //! `options::contract_math`: every settlement amount is a product of two //! integers, the only rounding is the floor in the fee split, and the expiry -//! window is one comparison and its complement. The harnesses prove the +//! window is one comparison and its complement. The harnesses check the //! invariants the program's custody accounting depends on, plus a bounded //! model of the vault ledger across an option's whole life. @@ -150,9 +154,9 @@ pub fn split_premium(premium: u64, fee_bps: u16) -> Option<(u64, u64)> { /// The premium is conserved: fee plus the writer's share is exactly the /// premium, the fee never exceeds the premium, and the writer always gets -/// something. Also proves the fee is the exact floor of `premium * bps / +/// something. Also checks the fee is the exact floor of `premium * bps / /// 10_000`, so a refactor that rounds up against the writer, or drops below -/// the floor against the venue, fails the proof. +/// the floor against the venue, fails the check. #[cfg(kani)] #[kani::proof] #[kani::solver(cadical)] diff --git a/finance/order-book/kani-proofs/Cargo.toml b/finance/order-book/kani-proofs/Cargo.toml index d507ee12e..4d6f7b804 100644 --- a/finance/order-book/kani-proofs/Cargo.toml +++ b/finance/order-book/kani-proofs/Cargo.toml @@ -2,7 +2,7 @@ # workspace. Kani (https://github.com/model-checking/kani) proof harnesses that # model the order-book's pure logic (the price-time matching engine, the # ceiling fee, the price-improvement rebate, and the lot/price conversions) so -# the model checker can verify the invariants without the Solana / SPL-token +# the model checker can check the invariants without the Solana / SPL-token # CPI machinery, which Kani cannot symbolically execute. [workspace] diff --git a/finance/order-book/kani-proofs/README.md b/finance/order-book/kani-proofs/README.md index 66f0e4999..712d218d3 100644 --- a/finance/order-book/kani-proofs/README.md +++ b/finance/order-book/kani-proofs/README.md @@ -1,18 +1,22 @@ -# Order-book: Kani proofs +# Order-book: Kani model checks -Formal-verification harnesses for the order-book program, in the spirit of -[`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +Kani harnesses that model-check the order-book program, in the spirit +of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`, +which is why the crate is `kani-proofs` and the harnesses are named `proof_*`; +each one is a model check: Kani tries every value of the inputs the harness +declares and reports either that every assertion held or an input that breaks +one. -## What is verified +## What is checked The on-chain instructions move tokens through SPL CPIs that Kani cannot symbolically execute, but the program's interesting logic (the price-time matching engine, the maker-funded ceiling fee, the taker's price-improvement rebate, and the two-lot price/quantity conversions) is pure integer -arithmetic. This crate reproduces those formulas faithfully and proves their -invariants: +arithmetic. This crate reproduces those formulas faithfully and checks their +invariants for every input: - `proof_matching_conserves_quantity`: **Matching conservation**: `total_filled + taker_remaining == incoming_quantity` (and so `place_order`'s `quantity.checked_sub(taker_remaining)` never underflows). - `proof_matching_respects_price_and_maker_size`: Every fill clears at a price that crosses the taker's limit and never exceeds the resting maker's size. @@ -22,9 +26,9 @@ invariants: ## Bounded model checking -The matching/bookkeeping proofs are pure linear logic and run at **full `u64` +The matching/bookkeeping harnesses are pure linear logic and run at **full `u64` width** (only the book depth is bounded, to 4 resting leaves via `unwind`). The -fee and rebate proofs verify **nonlinear 128-bit arithmetic** (`gross·bps`, and +fee and rebate harnesses check **nonlinear 128-bit arithmetic** (`gross·bps`, and the three-way `price·qty·lot` product), the hard case for a bit-precise solver, so (as percolator does) they bound their symbolic inputs to a representative range. The identities are scale-invariant, so the bounded domain still exercises @@ -36,15 +40,15 @@ every rounding / crossing boundary. - `proof_bid_rebate_is_non_negative`: prices/qty/lot `<= 31`, ~3s - `proof_remaining_quantity_consistent`: full `u64`, <1s -These proofs run **weekly in CI** (the `kani.yml` `verify` job), not on every -push/PR, because they are slow. A fast unit-test job runs per push/PR. +These model checks run **weekly in CI** (the `kani.yml` `verify` job), not on +every push/PR, because they are slow. A fast unit-test job runs per push/PR. ## Observations - The ceiling fee can make `fee == gross` on dust fills (e.g. `gross = 1`), so a maker can net zero quote on a sub-unit fill. This is intended (the comment in `place_order` notes ceiling rounding is in the protocol's favour to stop - fee-dust farming), not a bug: the proof confirms `fee <= gross` always holds, + fee-dust farming), not a bug: the model check confirms `fee <= gross` always holds, so the maker is never *overdrawn*. ## Running @@ -53,7 +57,7 @@ push/PR, because they are slow. A fast unit-test job runs per push/PR. # Plain unit tests (no Kani required): cargo test -# Formal verification (requires Kani): +# Kani model checks (requires Kani): cargo install --locked kani-verifier && cargo kani setup # one-time cargo kani ``` diff --git a/finance/order-book/kani-proofs/src/lib.rs b/finance/order-book/kani-proofs/src/lib.rs index 4fa4807cd..999b0ded4 100644 --- a/finance/order-book/kani-proofs/src/lib.rs +++ b/finance/order-book/kani-proofs/src/lib.rs @@ -1,7 +1,10 @@ -//! Kani proof harnesses for the order-book program (`finance/order-book`). +//! Kani harnesses for the order-book program (`finance/order-book`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check the arithmetic of a DeFi engine's pure numeric core. Kani marks a +//! harness with `#[kani::proof]`, which is why the crate is `kani-proofs` and +//! the harnesses are named `proof_*`; each one is a model check over every value +//! of the inputs it declares. //! //! The on-chain instructions move tokens through SPL CPIs that Kani cannot //! symbolically execute, but the program's *interesting* logic is pure: @@ -13,7 +16,7 @@ //! //! This crate reproduces those formulas faithfully (same `u128` widening, //! multiply-before-divide, ceiling rounding, `min` / `saturating_sub`) and -//! proves the invariants the program depends on. Several harnesses verify +//! checks the invariants the program depends on. Several harnesses check //! nonlinear 128-bit arithmetic, so — as percolator does — they use bounded //! model checking: symbolic inputs are constrained to a representative range so //! the bit-precise solver stays fast. The identities are scale-invariant, so a @@ -98,8 +101,8 @@ fn proof_matching_conserves_quantity() { } /// Every emitted fill clears at a price that crosses the taker's limit, and -/// never fills more than the resting leaf holds. Verified by re-walking the -/// book and checking each step (the model `break`s on the first non-crosser, +/// never fills more than the resting leaf holds. The harness re-walks the +/// book and checks each step (the model `break`s on the first non-crosser, /// exactly like `plan_fills`). #[cfg(kani)] #[kani::proof] diff --git a/finance/perpetual-futures/anchor-v1/README.md b/finance/perpetual-futures/anchor-v1/README.md index 7f9c54e09..9616d0165 100644 --- a/finance/perpetual-futures/anchor-v1/README.md +++ b/finance/perpetual-futures/anchor-v1/README.md @@ -21,7 +21,7 @@ A [perpetual future](https://www.investopedia.com/terms/f/futurescontract.asp) ( - `perpetual-futures`: The exchange: pool creation, liquidity provision, opening/closing leveraged positions, funding, liquidation, and fee collection. - `mock-price-feed`: Test-only price feed. Stores a price, scale, last-update slot, and confidence band that tests write directly. Replaced in production by a Pyth `PriceUpdateV2` account, as read in [`basics/pyth`](../../../basics/pyth/). -All money math is integer `u128` with `checked_*` operations, multiplying before dividing and rounding in the pool's favour: no floats, no fixed-point library. +All arithmetic is integer `u128` with `checked_*` operations, multiplying before dividing and rounding in the pool's favour: no floats, no fixed-point library. --- @@ -189,7 +189,7 @@ Carol burns her shares and redeems USDC. Her balance now reflects the fees the p ## Design notes and further reading -The genuinely hard part of a perpetual-futures venue is keeping it solvent and permissionless *without* re-evaluating the entire market on every action. For a rigorous, formally-verified (Kani) treatment, see Anatoly Yakovenko's [percolator](https://github.com/aeyakovenko/percolator), an educational perp risk engine. It states three invariants this example also leans on, in simplified form: +The genuinely hard part of a perpetual-futures venue is keeping it solvent and permissionless *without* re-evaluating the entire market on every action. For a rigorous, Kani-checked treatment, see Anatoly Yakovenko's [percolator](https://github.com/aeyakovenko/percolator), an educational perp risk engine. It states three invariants this example also leans on, in simplified form: - **Realizable credit**: "protected principal is senior, positive PnL is junior, and source-domain positive credit cannot exceed realizable backing reserved for that domain." Here, provider capital is senior and trader profit is a junior claim against it: shares are priced against marked assets-under-management, and the pool reserves each position's payout up front (capping recoverable profit at the reserve) so a winner's price profit can always be paid. - **Account-local safety**: "every favorable action refreshes the account's full active portfolio first; … stale … legs fail closed." Here, every position and liquidity action reads a fresh oracle (stale or wide-confidence prices are rejected) and recomputes pool exposure before any payout. diff --git a/finance/perpetual-futures/anchor/README.md b/finance/perpetual-futures/anchor/README.md index 92ea43dd4..e8040ea34 100644 --- a/finance/perpetual-futures/anchor/README.md +++ b/finance/perpetual-futures/anchor/README.md @@ -21,7 +21,7 @@ A [perpetual future](https://www.investopedia.com/terms/f/futurescontract.asp) ( - `perpetual-futures`: The exchange: pool creation, liquidity provision, opening/closing leveraged positions, funding, liquidation, and fee collection. - `mock-price-feed`: Test-only price feed. Stores a price, scale, last-update slot, and confidence band that tests write directly. Replaced in production by a Pyth `PriceUpdateV2` account, as read in [`basics/pyth`](../../../basics/pyth/). -All money math is integer `u128` with `checked_*` operations, multiplying before dividing and rounding in the pool's favour: no floats, no fixed-point library. +All arithmetic is integer `u128` with `checked_*` operations, multiplying before dividing and rounding in the pool's favour: no floats, no fixed-point library. --- @@ -189,7 +189,7 @@ Carol burns her shares and redeems USDC. Her balance now reflects the fees the p ## Design notes and further reading -The genuinely hard part of a perpetual-futures venue is keeping it solvent and permissionless *without* re-evaluating the entire market on every action. For a rigorous, formally-verified (Kani) treatment, see Anatoly Yakovenko's [percolator](https://github.com/aeyakovenko/percolator), an educational perp risk engine. It states three invariants this example also leans on, in simplified form: +The genuinely hard part of a perpetual-futures venue is keeping it solvent and permissionless *without* re-evaluating the entire market on every action. For a rigorous, Kani-checked treatment, see Anatoly Yakovenko's [percolator](https://github.com/aeyakovenko/percolator), an educational perp risk engine. It states three invariants this example also leans on, in simplified form: - **Realizable credit**: "protected principal is senior, positive PnL is junior, and source-domain positive credit cannot exceed realizable backing reserved for that domain." Here, provider capital is senior and trader profit is a junior claim against it: shares are priced against marked assets-under-management, and the pool reserves each position's payout up front (capping recoverable profit at the reserve) so a winner's price profit can always be paid. - **Account-local safety**: "every favorable action refreshes the account's full active portfolio first; … stale … legs fail closed." Here, every position and liquidity action reads a fresh oracle (stale or wide-confidence prices are rejected) and recomputes pool exposure before any payout. diff --git a/finance/perpetual-futures/quasar/src/instructions/shared.rs b/finance/perpetual-futures/quasar/src/instructions/shared.rs index 8dccb52ce..8cd13d5d5 100644 --- a/finance/perpetual-futures/quasar/src/instructions/shared.rs +++ b/finance/perpetual-futures/quasar/src/instructions/shared.rs @@ -1,4 +1,4 @@ -//! Money math and the oracle decode, ported verbatim from the Anchor sibling. +//! Arithmetic and the oracle decode, ported verbatim from the Anchor sibling. //! All integer, all `checked_*`, multiply-before-divide, rounding toward the //! protocol. Errors are `ProgramError::Custom(code)`; the codes are listed here. diff --git a/finance/prop-amm/kani-proofs/Cargo.toml b/finance/prop-amm/kani-proofs/Cargo.toml index a2adfe6bb..b5afbd536 100644 --- a/finance/prop-amm/kani-proofs/Cargo.toml +++ b/finance/prop-amm/kani-proofs/Cargo.toml @@ -1,7 +1,7 @@ # Standalone workspace - intentionally NOT part of the root program-examples # workspace. Kani (https://github.com/model-checking/kani) proof harnesses that # model the prop AMM's pure quoting arithmetic (ask/bid construction, output -# amounts, the oracle-value invariant) so the model checker can verify the +# amounts, the oracle-value invariant) so the model checker can check the # invariants without the Solana / SPL-token CPI machinery, which Kani cannot # symbolically execute. [workspace] diff --git a/finance/prop-amm/kani-proofs/README.md b/finance/prop-amm/kani-proofs/README.md index 73c7d994e..758287d01 100644 --- a/finance/prop-amm/kani-proofs/README.md +++ b/finance/prop-amm/kani-proofs/README.md @@ -1,11 +1,15 @@ -# Prop AMM: Kani proofs +# Prop AMM: Kani model checks -Formal-verification harnesses for the oracle-quoted prop AMM, in the spirit of +Kani harnesses for the oracle-quoted prop AMM, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. Kani marks a harness with `#[kani::proof]`, +which is why the crate is `kani-proofs` and the harnesses are named `proof_*`; +each one is a model check: Kani tries every value of the inputs the harness +declares and reports either that every assertion held or the input that breaks +one. -## What is verified +## What is checked The on-chain instructions hand token movement to the SPL token program through CPIs that Kani cannot symbolically execute, but the *interesting* part — the @@ -13,18 +17,19 @@ ask/bid construction, the amount conversion across oracle scale and token decimals, and the "never pay out more than oracle value" invariant — is pure integer arithmetic. This crate reproduces those formulas faithfully (same `u128` widening, multiply-before-divide, ask ceiled, bid and outputs floored; -mirrors `prop_amm::quote_math`) and proves the invariants: +mirrors `prop_amm::quote_math`) and checks the invariants for every input in +the declared ranges: - `proof_quote_brackets_oracle`: `bid <= oracle <= ask` for every valid price and spread, and both roundings are *exact* (the ask is the smallest integer at or above the true ratio, the bid the largest at or below), so both under-rounding against the market and over-rounding against the trader fail - the proof. + the check. - `proof_buy_never_exceeds_oracle_value`: **The core safety property**, buy side: the base handed out is never worth more at the raw oracle price than the quote taken in. This is exactly the swap handler's post-math - `InvariantViolated` assert — the proof says it can never fire while the - quoting math is intact. + `InvariantViolated` assert; the model check shows it cannot fire for any + input in range while the quoting math is intact. - `proof_sell_never_exceeds_oracle_value`: the same property, sell side. - `proof_round_trip_never_profits_the_trader`: buying and immediately selling back returns no more quote than went in, for every price, spread, and @@ -53,6 +58,6 @@ valid range (`1..10_000`). # tests and the book chapter use: cargo test -# Full verification (requires cargo-kani): +# Full model check (requires cargo-kani): cargo kani ``` diff --git a/finance/prop-amm/kani-proofs/src/lib.rs b/finance/prop-amm/kani-proofs/src/lib.rs index 3973c7d2e..316cf4452 100644 --- a/finance/prop-amm/kani-proofs/src/lib.rs +++ b/finance/prop-amm/kani-proofs/src/lib.rs @@ -1,7 +1,11 @@ -//! Kani proof harnesses for the prop AMM (`finance/prop-amm`). +//! Kani harnesses for the prop AMM (`finance/prop-amm`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check a DeFi engine's pure numeric core. Kani marks a harness with +//! `#[kani::proof]`, which is why the crate is `kani-proofs` and the harnesses +//! are named `proof_*`; each one is a model check: Kani tries every value of +//! the inputs the harness declares and reports either that every assertion +//! held or the input that breaks one. //! //! The on-chain instructions hand the actual token movement to the SPL token //! program via CPIs that Kani cannot symbolically execute. But the @@ -10,7 +14,7 @@ //! "never pay out more than oracle value" invariant — is pure integer //! arithmetic. This crate reproduces those formulas faithfully (same `u128` //! widening, same multiply-before-divide, same rounding directions: ask ceils, -//! bid floors, outputs floor) and proves the invariants the program depends +//! bid floors, outputs floor) and checks the invariants the program depends //! on. Formulas mirror `prop_amm::quote_math`. #![cfg_attr(kani, allow(dead_code))] @@ -39,10 +43,10 @@ pub fn bid_price(oracle_price: u64, spread_bps: u16) -> Option { } /// The quote brackets the oracle: `bid <= oracle <= ask`, with each side's -/// rounding pointing away from the trader. Also proves the roundings are +/// rounding pointing away from the trader. Also checks the roundings are /// exact: the ask is the *smallest* integer at or above the true ratio (ceil, /// not "add one"), so a refactor that over-rounds in the market's favor fails -/// the proof too. +/// the check too. #[cfg(kani)] #[kani::proof] #[kani::solver(cadical)] @@ -126,8 +130,8 @@ pub fn quote_out_for_base_in( /// THE core prop-AMM safety property, buy side: the base handed out is never /// worth more, at the raw oracle price, than the quote taken in — for every /// price, spread, amount, and decimal configuration. This is exactly the -/// `require!(respects_oracle_value)` assert in the swap handler; the proof -/// says that assert can never fire while the math above it is intact. +/// `require!(respects_oracle_value)` assert in the swap handler; the model +/// check shows that assert can never fire while the math above it is intact. #[cfg(kani)] #[kani::proof] #[kani::solver(cadical)] @@ -143,7 +147,7 @@ fn proof_buy_never_exceeds_oracle_value() { // part for the bit-precise solver, and its cost grows with the divisor's // bit-width (ask spans one more bit than price). Amounts and price are // capped at 8 bits — in line with the symbolic-divisor bounds the other - // finance proof crates stay tractable with — and the decimal exponents + // finance Kani crates stay tractable with — and the decimal exponents // are kept small (the identity is independent of the exponents' actual // values — they enter both sides of the comparison symmetrically — so // tiny exponents exercise the same rounding edges as scale 8 and 6/6 diff --git a/finance/token-swap/anchor-v1/README.md b/finance/token-swap/anchor-v1/README.md index 9e48aa66f..896b221dc 100644 --- a/finance/token-swap/anchor-v1/README.md +++ b/finance/token-swap/anchor-v1/README.md @@ -52,4 +52,4 @@ An automated market maker replaces the order book with a liquidity pool: anyone ### Where is the full walkthrough for this example? -The example-level [Token Swap overview](../README.md) covers the pool math, LP tokens, and lifecycle; this page covers the Anchor build and test commands. The money math has [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/). +The example-level [Token Swap overview](../README.md) covers the pool math, LP tokens, and lifecycle; this page covers the Anchor build and test commands. The arithmetic has [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/). diff --git a/finance/token-swap/anchor/README.md b/finance/token-swap/anchor/README.md index 11894f5a5..5dfc65d02 100644 --- a/finance/token-swap/anchor/README.md +++ b/finance/token-swap/anchor/README.md @@ -52,4 +52,4 @@ An automated market maker replaces the order book with a liquidity pool: anyone ### Where is the full walkthrough for this example? -The example-level [Token Swap overview](../README.md) covers the pool math, LP tokens, and lifecycle; this page covers the Anchor build and test commands. The money math has [Kani](https://github.com/model-checking/kani) proofs in [`../kani-proofs/`](../kani-proofs/). +The example-level [Token Swap overview](../README.md) covers the pool math, LP tokens, and lifecycle; this page covers the Anchor build and test commands. The arithmetic has [Kani](https://github.com/model-checking/kani) model checks in [`../kani-proofs/`](../kani-proofs/). diff --git a/finance/token-swap/kani-proofs/Cargo.toml b/finance/token-swap/kani-proofs/Cargo.toml index 7656c3a52..30141dd1e 100644 --- a/finance/token-swap/kani-proofs/Cargo.toml +++ b/finance/token-swap/kani-proofs/Cargo.toml @@ -1,7 +1,7 @@ # Standalone workspace - intentionally NOT part of the root program-examples # workspace. Kani (https://github.com/model-checking/kani) proof harnesses that # model the AMM's pure arithmetic (constant-product curve, fee split, integer -# sqrt, proportional withdraw) so the model checker can verify the invariants +# sqrt, proportional withdraw) so the model checker can check the invariants # without the Solana / SPL-token CPI machinery, which Kani cannot symbolically # execute. [workspace] diff --git a/finance/token-swap/kani-proofs/README.md b/finance/token-swap/kani-proofs/README.md index ca9438c8c..edc0b1da7 100644 --- a/finance/token-swap/kani-proofs/README.md +++ b/finance/token-swap/kani-proofs/README.md @@ -1,23 +1,28 @@ -# Token-swap (AMM): Kani proofs +# Token-swap (AMM): Kani model checks -Formal-verification harnesses for the constant-product AMM, in the spirit of +Kani model-check harnesses for the constant-product AMM, in the spirit of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which -uses the [Kani](https://github.com/model-checking/kani) model checker to prove -the mathematical correctness of a DeFi engine. +uses the [Kani](https://github.com/model-checking/kani) model checker to check +the arithmetic of a DeFi engine. -## What is verified +Kani marks a harness with `#[kani::proof]`, which is why the crate is +`kani-proofs` and the harnesses are named `proof_*`; each one is a model check: +it tries every value of its declared inputs and reports either that every +assertion held or the input that breaks one. + +## What is checked The on-chain instructions hand token movement to the SPL token program through CPIs that Kani cannot symbolically execute, but the *interesting* part, the constant-product curve, the fee split, the integer square root used for the initial LP mint, and the proportional deposit and withdraw math, is pure integer arithmetic. This crate reproduces those formulas faithfully (same `u128` -widening, multiply-before-divide, floor rounding) and proves their invariants: +widening, multiply-before-divide, floor rounding) and checks their invariants: - `proof_fee_split_bounds`: `fee <= input`, `admin_portion <= fee`, and `taxed_input + fee == input`. - `proof_swap_preserves_constant_product`: **The core safety property**: a swap never decreases `k = reserve_in * reserve_out`. - `proof_swap_cannot_fully_drain_when_reserve_positive`: With a non-empty input reserve, output is always `< other_reserve` (pool stays solvent). -- `proof_swap_at_zero_reserve_drains_whole_pool`: **Finding**, proven as a positive characterization (see below). +- `proof_swap_at_zero_reserve_drains_whole_pool`: **Finding**, checked as a positive characterization (see below). - `proof_integer_sqrt_is_floor`: `integer_sqrt` returns the exact floor: `r² <= n < (r+1)²`. - `proof_withdraw_never_exceeds_reserve`: An LP can never withdraw more than the reserve holds (the `MINIMUM_LIQUIDITY` floor guarantees it). - `proof_deposit_withdraw_round_trip_is_fair`: Burning the LP tokens a deposit just minted returns at most the deposit, and less than one minor unit plus one LP token's worth short of it. The lower bound holds only because deposit and withdraw both divide by `lp_supply + MINIMUM_LIQUIDITY`; a deposit divided by the bare supply fails it. @@ -26,13 +31,13 @@ widening, multiply-before-divide, floor rounding) and proves their invariants: ## Bounded model checking -Several harnesses verify **nonlinear 128-bit arithmetic** (e.g. +Several harnesses check **nonlinear 128-bit arithmetic** (e.g. `reserve_in * reserve_out`, and worst of all `amount * pool_b / pool_a` where the *divisor* is symbolic), the hardest case for a bit-precise model checker. Kani bit-blasts the full multiplier/divider into SAT. Following percolator's own practice (it bounds inputs to ranges like `±500`), these harnesses constrain their symbolic inputs to a representative range so the solver stays fast. The -identities being proven are scale-invariant, so the bounded domain still +identities being checked are scale-invariant, so the bounded domain still exercises every rounding boundary. The bound is per-harness, sized to its difficulty: @@ -46,9 +51,9 @@ difficulty: - `proof_rounding_a_deposit_to_zero_needs_floor_times_donation`: deposit and attacker LP `<= 15`, reserve `<= 4095`, runs in ~2s - `proof_deposit_clamp_never_exceeds_request`: `<= 31` (symbolic divisor), runs in ~3s -The whole suite verifies in about two minutes of solver time. This is why these proofs run -**weekly in CI** (the `kani.yml` `verify` job), not on every push/PR. A fast -unit-test job runs per push/PR. +The whole suite runs in about two minutes of solver time. This is why these +model checks run **weekly in CI** (the `kani.yml` `verify` job), not on every +push/PR. A fast unit-test job runs per push/PR. ## Finding (now fixed): full drain at a zero effective reserve @@ -77,7 +82,7 @@ positive, and `proof_swap_preserves_constant_product` shows ordinary swaps keep both sides positive), so this was a latent edge, not a live exploit, but the guard means solvency no longer *depends* on that argument. -The harness is kept as a **positive** proof (every assertion holds: `output == +The harness is kept as a **positive** model check (every assertion holds: `output == other_reserve` and `0 >= 0`) characterizing the raw `swap_output` formula at the boundary, which is exactly the justification for the program guard. It is not a `#[kani::should_panic]`, which would have started failing the moment the @@ -89,7 +94,7 @@ boundary, which is exactly the justification for the program guard. It is not a # Plain unit tests (no Kani required): cargo test -# Formal verification (requires Kani): +# Kani model checks (requires Kani): cargo install --locked kani-verifier && cargo kani setup # one-time cargo kani ``` diff --git a/finance/token-swap/kani-proofs/src/lib.rs b/finance/token-swap/kani-proofs/src/lib.rs index 8444842fd..90e51f9d2 100644 --- a/finance/token-swap/kani-proofs/src/lib.rs +++ b/finance/token-swap/kani-proofs/src/lib.rs @@ -1,7 +1,12 @@ -//! Kani proof harnesses for the constant-product AMM (`finance/token-swap`). +//! Kani model-check harnesses for the constant-product AMM +//! (`finance/token-swap`). //! //! Inspired by aeyakovenko/percolator, which uses the Kani model checker to -//! prove the mathematical correctness of a DeFi engine's pure numeric core. +//! check the arithmetic of a DeFi engine's pure numeric core. +//! +//! Kani marks a harness with `#[kani::proof]`, which is why the crate is +//! `kani-proofs` and the harnesses are named `proof_*`; each one is a model +//! check, which tries every value of its declared inputs, not a formal proof. //! //! The on-chain instructions (`swap_tokens`, `deposit_liquidity`, //! `withdraw_liquidity`) hand the actual token movement to the SPL token @@ -10,7 +15,7 @@ //! used for the initial LP mint, and the proportional deposit and withdraw //! math — is pure integer arithmetic. This crate reproduces those formulas //! faithfully (same `u128` widening, same multiply-before-divide, same floor -//! rounding) and proves the invariants the program depends on. +//! rounding) and checks the invariants the program depends on. //! //! Constants mirror `constants.rs`. @@ -96,7 +101,7 @@ pub fn swap_output(taxed_input: u64, this_reserve: u64, other_reserve: u64) -> O /// /// This models the full reserve transition the on-chain `require!(new_invariant /// >= invariant)` checks: the input side grows by `taxed_input` plus the LP -/// slice of the fee (`lp_fee`), the output side shrinks by `output`. We prove +/// slice of the fee (`lp_fee`), the output side shrinks by `output`. We check /// the post-trade product dominates the pre-trade product for *every* reserve /// configuration and input — the model checker's analogue of "the pool can /// never be drained below the curve". @@ -109,10 +114,10 @@ fn proof_swap_preserves_constant_product() { let taxed_input: u64 = kani::any(); let lp_fee: u64 = kani::any(); // fee_amount - admin_portion, stays in pool - // Bounded model checking: this proof multiplies two symbolic reserves + // Bounded model checking: this harness multiplies two symbolic reserves // (`new_in * new_out`), the worst case for a bit-precise solver. Cap each - // quantity at 1023 so the four-variable nonlinear search stays fast; the - // algebraic identity it verifies — (ra+t)(rb-floor(t*rb/(ra+t))) >= ra*rb — + // quantity at 63 so the four-variable nonlinear search stays fast; the + // algebraic identity it checks, (ra+t)(rb-floor(t*rb/(ra+t))) >= ra*rb, // is scale-invariant, so the bounded domain exercises the same rounding // edges as the full u64 range. kani::assume(reserve_in <= 63); @@ -127,7 +132,7 @@ fn proof_swap_preserves_constant_product() { // Reserve transition (effective reserves): let new_in = reserve_in as u128 + taxed_input as u128 + lp_fee as u128; - let new_out = reserve_out as u128 - output as u128; // proves output <= reserve_out (no underflow) + let new_out = reserve_out as u128 - output as u128; // checks output <= reserve_out (no underflow) let old_k = (reserve_in as u128) * (reserve_out as u128); let new_k = new_in * new_out; @@ -155,7 +160,7 @@ fn proof_swap_cannot_fully_drain_when_reserve_positive() { assert!(output < other_reserve, "output must leave the pool solvent"); } -/// FINDING (now FIXED in the program) — this proof is the justification for the +/// FINDING (now FIXED in the program) — this harness is the justification for the /// fix. It characterizes *why* `swap_tokens` must reject empty reserves: when an /// input-side effective reserve is exactly `0`, the curve outputs the ENTIRE /// opposite reserve (`output == other_reserve`), draining that side — and the @@ -171,16 +176,17 @@ fn proof_swap_cannot_fully_drain_when_reserve_positive() { /// already make it unreachable in normal operation; the guard means solvency no /// longer *depends* on that reachability argument. /// -/// We keep this as a *positive* proof (every assertion below holds) characterizing -/// the raw `swap_output` formula at the boundary — not a `#[kani::should_panic]`, -/// which would have started failing the moment the `require!` fix landed. +/// We keep this as a *positive* model check (every assertion below holds) +/// characterizing the raw `swap_output` formula at the boundary — not a +/// `#[kani::should_panic]`, which would have started failing the moment the +/// `require!` fix landed. #[cfg(kani)] #[kani::proof] #[kani::solver(cadical)] fn proof_swap_at_zero_reserve_drains_whole_pool() { let other_reserve: u64 = kani::any(); let taxed_input: u64 = kani::any(); - // Bounded model checking: proving `floor(taxed*other/taxed) == other` for all + // Bounded model checking: checking `floor(taxed*other/taxed) == other` for all // inputs is a symbolic exact-division (divisor == a factor of the numerator), // costlier than the old refute-by-counterexample form, so bound tightly. kani::assume(other_reserve >= 1 && other_reserve <= 255); @@ -204,7 +210,7 @@ fn proof_swap_at_zero_reserve_drains_whole_pool() { /// Verbatim copy of `deposit_liquidity::integer_sqrt` (Newton's method, floor). /// -/// Only the `#[cfg(kani)]` proof and the unit tests call it, so a plain +/// Only the `#[cfg(kani)]` harness and the unit tests call it, so a plain /// `cargo build` of the library sees no caller. #[allow(dead_code)] fn integer_sqrt(n: u128) -> u128 { @@ -237,7 +243,7 @@ fn proof_integer_sqrt_is_floor() { // 128-bit division (`n / x`) in its body, which the model checker must // unroll and bit-blast — the single most expensive shape for a SAT // backend. Capping `n` at 255 keeps the unroll short (<=10 iterations, so - // `unwind(11)` proves termination) and the `r*r` / `(r+1)*(r+1)` products + // `unwind(11)` checks termination) and the `r*r` / `(r+1)*(r+1)` products // small, while still exercising every floor-rounding boundary up to r = 15. kani::assume(n <= 255); @@ -424,7 +430,7 @@ fn proof_deposit_clamp_never_exceeds_request() { // Bound them tightly to stay tractable; the clamp identity is scale-free. kani::assume(amount_a <= 31 && amount_b <= 31); // Existing pool: both reserves non-zero (the pool-creation branch is the - // trivial identity, proven by construction). + // trivial identity, so this harness does not check it). kani::assume(pool_a >= 1 && pool_a <= 31); kani::assume(pool_b >= 1 && pool_b <= 31); diff --git a/llms.txt b/llms.txt index 4b1169a20..d8dec543a 100644 --- a/llms.txt +++ b/llms.txt @@ -1,6 +1,6 @@ # Solana Program Examples -> Working, tested, up-to-date Solana program ('smart contract') examples, maintained by Quicknode. Focused on financial software ('DeFi'): every finance example ships LiteSVM integration tests and Kani formal-verification proofs of its money math, and builds in CI on Anchor 1.2. Most examples are available in several frameworks: Anchor, Quasar, Pinocchio, native Rust, and sBPF assembly. +> Working, tested, up-to-date Solana program ('smart contract') examples, maintained by Quicknode. Focused on financial software ('DeFi'): every finance example ships LiteSVM integration tests and Kani formal-verification proofs of its arithmetic, and builds in CI on Anchor 1.2. Most examples are available in several frameworks: Anchor, Quasar, Pinocchio, native Rust, and sBPF assembly. A Solana program is what other chains call a smart contract. These examples are reference implementations for learning: tested and formally verified, but not audited or deployed to mainnet. @@ -26,4 +26,4 @@ A Solana program is what other chains call a smart contract. These examples are ## Testing and verification - Tests are Rust integration tests against [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm), run with `cargo test`; no local validator is needed. -- Every finance example has a `kani-proofs/` directory with [Kani](https://github.com/model-checking/kani) harnesses proving money-math invariants over all inputs, for example [escrow's proofs](https://github.com/quicknode/solana-program-examples/tree/main/finance/escrow/kani-proofs). +- Every finance example has a `kani-proofs/` directory with [Kani](https://github.com/model-checking/kani) harnesses proving arithmetic invariants over all inputs, for example [escrow's proofs](https://github.com/quicknode/solana-program-examples/tree/main/finance/escrow/kani-proofs). diff --git a/tokens/quasar-metadata/src/instructions/mod.rs b/tokens/quasar-metadata/src/instructions/mod.rs index 42c04ec1c..f120fedd2 100644 --- a/tokens/quasar-metadata/src/instructions/mod.rs +++ b/tokens/quasar-metadata/src/instructions/mod.rs @@ -637,7 +637,7 @@ impl MetadataCpi for crate::MetadataProgram {} impl MetadataCpi for AccountView {} // --------------------------------------------------------------------------- -// Kani proof harnesses for Metaplex metadata instruction data layout +// Kani model-check harnesses for Metaplex metadata instruction data layout // --------------------------------------------------------------------------- // // Each harness replicates the unsafe `MaybeUninit` + pointer-write pattern used