Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions basics/account-data/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: the [repository catalog](../../../README.md).
From this directory (`basics/account-data/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/checking-accounts/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Checking Accounts overview](../README.md) and the [repository catalog
From this directory (`basics/checking-accounts/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
3 changes: 1 addition & 2 deletions basics/close-account/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@ Two [instruction handlers](https://solana.com/docs/terminology#instruction-handl
## Setup

```bash
pnpm install
anchor build
```

Expand All @@ -43,5 +42,5 @@ anchor build
Tests live in [`programs/close-account/tests/test_close_account.rs`](programs/close-account/tests/test_close_account.rs) and run in-process with LiteSVM:

```bash
pnpm test
anchor test
```
3 changes: 1 addition & 2 deletions basics/counter/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,13 @@ See also: the [repository catalog](../../README.md).
From `basics/counter/anchor/`:

```bash
pnpm install
anchor build
```

## Testing

```bash
pnpm test
anchor test
```

LiteSVM integration tests in `programs/counter_anchor/tests/` call handlers and assert the stored count.
Expand Down
5 changes: 2 additions & 3 deletions basics/create-account/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Create Account overview](../README.md) and the [repository catalog](.
From this directory (`basics/create-account/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/cross-program-invocation/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Cross Program Invocation overview](../README.md) and the [repository
From this directory (`basics/cross-program-invocation/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/favorites/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,18 +12,17 @@ See also: the [repository catalog](../../README.md).
## Setup

```bash
pnpm install
anchor build
```

## Testing

```bash
pnpm test
anchor test
```

LiteSVM tests in `programs/` assert that users cannot overwrite each other's state.

## Usage

`anchor deploy` targets the cluster in `Anchor.toml`. Used in [Solana Professional Education](https://github.com/solana-developers/professional-education).
`anchor deploy` targets the cluster in `Anchor.toml`.
5 changes: 2 additions & 3 deletions basics/hello-solana/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Hello Solana overview](../README.md) and the [repository catalog](../
From this directory (`basics/hello-solana/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/pda-rent-payer/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Pda Rent Payer overview](../README.md) and the [repository catalog](.
From this directory (`basics/pda-rent-payer/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/processing-instructions/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Processing Instructions overview](../README.md) and the [repository c
From this directory (`basics/processing-instructions/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/program-derived-addresses/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: the [repository catalog](../../../README.md).
From this directory (`basics/program-derived-addresses/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/pyth/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,18 +29,17 @@ See also: [Pyth overview](../README.md) and the [repository catalog](../../../RE
From this directory (`basics/pyth/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/realloc/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Realloc overview](../README.md) and the [repository catalog](../../..
From this directory (`basics/realloc/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/rent/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Rent overview](../README.md) and the [repository catalog](../../../RE
From this directory (`basics/rent/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/repository-layout/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Repository Layout overview](../README.md) and the [repository catalog
From this directory (`basics/repository-layout/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 2 additions & 3 deletions basics/transfer-sol/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,17 @@ See also: [Transfer Sol overview](../README.md) and the [repository catalog](../
From this directory (`basics/transfer-sol/anchor/`):

```bash
pnpm install
anchor build
```

Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs), and `pnpm`.
Prerequisites: [Agave](https://docs.anza.xyz/) CLI (version in `Anchor.toml` `[toolchain]`), [Anchor](https://www.anchor-lang.com/docs).

## Testing

Tests run in-process with [LiteSVM](https://www.anchor-lang.com/docs/testing/litesvm). No local validator.

```bash
pnpm test
anchor test
```

This runs `cargo test` as configured in `Anchor.toml`. Tests call instruction handlers and check onchain state.
Expand Down
5 changes: 3 additions & 2 deletions finance/betting-market/anchor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,9 @@ where odds are set by the crowd's stakes rather than by an order book or a fixed

## Purpose

It solves the core problem of trustless betting: collecting stakes from many bettors, holding them
in one place no single bettor controls, and paying winners by a fixed, public formula. The pool is
It solves the core custody problem of pooled betting: collecting stakes from many bettors, holding
them in one place no single bettor controls, and paying winners by a fixed, public formula. Resolution
still requires trusting the admin, who chooses the winning outcome, as described below. The pool is
a token account owned by the event's PDA, so payouts are signed by the program with the event's
seeds - there is no admin key that can move bettors' stakes out of the pool. The admin's only
powers are creating events/outcomes and choosing the winning outcome (or cancelling).
Expand Down
26 changes: 11 additions & 15 deletions finance/betting-market/kani-proofs/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Betting-market Kani proofs
# Betting-market: Kani proofs

Formal-verification harnesses for the pari-mutuel betting market, in the spirit
of [`aeyakovenko/percolator`](https://github.com/aeyakovenko/percolator), which
Expand All @@ -12,38 +12,34 @@ 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:

| Harness | Property |
| --- | --- |
| `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). |
| `proof_parimutuel_solvency` | **Solvency** (centrepiece): the winners collectively never claim more than the vault holds after the fee (`Σ payout_i <= winning_pool + distributable`). |
| `proof_refund_conserves_pool` | On cancellation, refunds sum back to the total pool — neither over- nor under-drained. |
- `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).
- `proof_parimutuel_solvency`: **Solvency** (centrepiece): the winners collectively never claim more than the vault holds after the fee (`Σ payout_i <= winning_pool + distributable`).
- `proof_refund_conserves_pool`: On cancellation, refunds sum back to the total pool, neither over- nor under-drained.

### The solvency proof

After settlement the vault holds `winning_pool + distributable_losing_pool`.
Each winner is paid `stake_i + floor(stake_i · D / winning_pool)`, and the
winning stakes sum to `winning_pool`. Because
`Σ floor(stake_i·D/W) <= Σ stake_i·D/W = D`, total payouts are
`<= winning_pool + D` exactly the vault balance. So no set of winners can drain
`<= winning_pool + D`, exactly the vault balance. So no set of winners can drain
the vault below zero; floor rounding only ever leaves dust behind. Modelled with
3 winners whose stakes sum to the winning pool.

## Bounded model checking

The settlement, payout, and solvency proofs verify 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
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
the number of bettors).

| Harness | Bound | Time |
| --- | --- | --- |
| `proof_settlement_fee_and_split` | `total_pool <= 4095`, `fee_bps` symbolic | ~1s |
| `proof_winner_never_below_stake` | `winning_pool/distributable <= 255` | ~6s |
| `proof_parimutuel_solvency` | 3 winners, stakes `<= 7`, `distributable <= 63` | ~3s |
| `proof_refund_conserves_pool` | 4 bettors, full `u64` | <1s |
- `proof_settlement_fee_and_split`: `total_pool <= 4095`, `fee_bps` symbolic, ~1s
- `proof_winner_never_below_stake`: `winning_pool/distributable <= 255`, ~6s
- `proof_parimutuel_solvency`: 3 winners, stakes `<= 7`, `distributable <= 63`, ~3s
- `proof_refund_conserves_pool`: 4 bettors, full `u64`, <1s

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.

Expand Down
Loading
Loading