---
name: proptest-invariant
description: Generate a proptest block for a named orderbook-rs matching-engine invariant. Use when adding coverage for invariants like "sum of resting quantity conserved", "maker.price == trade.price", "no trades with equal maker and taker under STP", "replay byte-identical via the sequencer", "price-time priority never violated", "no orders at zero quantity", or "snapshot restore round-trips". Generates strategies that go through the validated `pricelevel` newtypes (`Price`, `Quantity`, `Id`, `Side`, `TimeInForce`) and drives `OrderBook<T>` via the public `operations` / `modifications` / `mass_cancel` surface. Includes shrinking configuration tuned for short failing streams.
allowed-tools: Read, Write, Edit, Grep, Glob, Bash
---

# Skill: proptest-invariant

Generates a `proptest` block that targets a specific `orderbook-rs` matching-engine
invariant. The harness drives `OrderBook<T>` with a randomly generated, valid input
stream and asserts the invariant on the resulting state and emitted events.

## When to invoke

- Adding coverage for an invariant that currently has only example tests (or none).
- User says "property test for <invariant>", "proptest <invariant>", "add a proptest that
  <property holds>".
- After changing matching semantics, STP modes, fees, or the sequencer replay path —
  invariants should regrow coverage.

## Supported invariants (lookup table)

| Name                          | Shape                                                                 |
|-------------------------------|-----------------------------------------------------------------------|
| `qty_conserved`               | sum of resting qty on each side invariant under non-matching ops      |
| `no_zero_qty_levels`          | no resting order with `Quantity::ZERO`, no level with total qty zero  |
| `trade_has_one_maker_taker`   | every `TradeEvent` has 1 maker + 1 taker, `maker.price == trade.price`|
| `price_time_priority`         | fills consume older orders first within a price level                 |
| `stp_never_self_fills`        | no `TradeEvent` where maker and taker share the same owner id         |
| `replay_snapshots_match`      | sequencer replay produces `snapshots_match == true`                   |
| `bbo_matches_book`            | `PriceLevelCache` top-of-book reflects the actual best bid/ask        |
| `fees_per_fill_sum`           | total fee across fills equals sum of per-fill fees, no rounding drift |
| `snapshot_restore_roundtrip`  | `restore_from_snapshot_package` reproduces equivalent state           |

If the user asks for something not on this list, ask them to name which invariant and
where it lives in the public README or `lib.rs`; then add a row to the table in the same
commit as the test.

## Procedure

### 1. File placement

- Integration tests live at `tests/unit/props_<invariant>.rs` (one file per invariant
  group). They are driven via the public `OrderBook<T>` API only — no crate-internal
  imports.
- Shared input-stream strategies live at `tests/unit/common/strategies.rs`.
- Unit-level invariants that need crate-internal visibility go under
  `src/orderbook/tests/props_<invariant>.rs` gated by `#[cfg(test)]`.

Prefer the integration-test location when the public API covers the invariant; `proptest`
integration tests run under `cargo nextest run --test props_<invariant>` in isolation,
which makes shrink failures easier to reproduce.

### 2. Template — the stream strategy

Reusable generator for a sequence of valid operations. Biased to produce crossings often
enough to exercise matching, not uniformly random.

```rust
// tests/unit/common/strategies.rs

use orderbook_rs::prelude::*;
use proptest::prelude::*;
use proptest::collection::vec;

/// Small, deterministic set of owner ids. Keeping the pool small makes STP / self-cross
/// exercise frequently on short streams.
const OWNER_POOL: [u64; 4] = [1, 2, 3, 4];

/// Operation generated by the strategy. Keep this enum local to the test crate so it
/// does not get re-exported by accident.
#[derive(Clone, Debug)]
pub enum Op {
    Submit {
        id: Id,
        owner: u64,
        side: Side,
        price: Price,
        qty: Quantity,
        tif: TimeInForce,
    },
    CancelById(Id),
    MassCancelBySide(Side),
}

pub fn op_stream(len_range: std::ops::Range<usize>) -> impl Strategy<Value = Vec<Op>> {
    vec(op(), len_range)
}

fn op() -> impl Strategy<Value = Op> {
    prop_oneof![
        7 => submit(),
        2 => cancel(),
        1 => mass_cancel(),
    ]
}

fn submit() -> impl Strategy<Value = Op> {
    (
        any::<u64>().prop_map(Id::from_u64),
        any::<usize>().prop_map(|i| OWNER_POOL[i % OWNER_POOL.len()]),
        any::<Side>(),
        // Tight price band forces crossings. A wide uniform range produces a flat empty
        // book that never exercises matching.
        (99u64..=101).prop_map(|t| Price::from_u64(t)),
        (1u64..=100).prop_map(|q| Quantity::from_u64(q)),
        tif_any(),
    )
        .prop_map(|(id, owner, side, price, qty, tif)| Op::Submit {
            id, owner, side, price, qty, tif,
        })
}

fn cancel() -> impl Strategy<Value = Op> {
    any::<u64>().prop_map(|v| Op::CancelById(Id::from_u64(v)))
}

fn mass_cancel() -> impl Strategy<Value = Op> {
    prop_oneof![
        Just(Op::MassCancelBySide(Side::Buy)),
        Just(Op::MassCancelBySide(Side::Sell)),
    ]
}

fn tif_any() -> impl Strategy<Value = TimeInForce> {
    prop_oneof![
        Just(TimeInForce::Gtc),
        Just(TimeInForce::Ioc),
        Just(TimeInForce::Fok),
        Just(TimeInForce::PostOnly),
    ]
}
```

Key points:

- **Bias weights** (`prop_oneof![7 => …, 2 => …]`) matter. Uniform random rarely exercises
  cancels or STP paths in a short run.
- **Tight price band** forces crossings. Uniform prices over the full range produce a
  flat empty book.
- **Small owner pool** makes self-crosses frequent enough to exercise every STP mode.
- Strategy only emits values that pass through the validated constructors (`Price`,
  `Quantity`) — invalid inputs belong in their own test.

### 3. Template — an invariant test

Example for `qty_conserved` (replace `<OrderBookCtor>` with the exact constructor used in
the project, typically `OrderBook::<()>::new("TEST")` or a preset builder):

```rust
// tests/unit/props_qty_conserved.rs

mod common;
use common::strategies::{op_stream, Op};

use orderbook_rs::prelude::*;
use proptest::prelude::*;

fn apply(book: &OrderBook<()>, op: &Op) {
    match op {
        Op::Submit { id, owner, side, price, qty, tif } => {
            let _ = book.submit_limit(*id, *owner, *side, *price, *qty, *tif);
        }
        Op::CancelById(id) => {
            let _ = book.cancel(*id);
        }
        Op::MassCancelBySide(side) => {
            let _ = book.mass_cancel_by_side(*side);
        }
    }
}

fn bid_qty_sum(book: &OrderBook<()>) -> u64 {
    book.iter_levels(Side::Buy)
        .map(|lvl| lvl.total_quantity().as_u64())
        .sum()
}

fn ask_qty_sum(book: &OrderBook<()>) -> u64 {
    book.iter_levels(Side::Sell)
        .map(|lvl| lvl.total_quantity().as_u64())
        .sum()
}

proptest! {
    #![proptest_config(ProptestConfig {
        cases: 256,
        max_shrink_iters: 50_000,
        ..ProptestConfig::default()
    })]

    #[test]
    fn qty_conserved_across_snapshot(stream in op_stream(1..200)) {
        let book = OrderBook::<()>::new("TEST");
        for op in &stream { apply(&book, op); }

        let bid_before = bid_qty_sum(&book);
        let ask_before = ask_qty_sum(&book);

        // Non-matching op: snapshot must not change resting qty.
        let _snap = book.snapshot();

        prop_assert_eq!(bid_qty_sum(&book), bid_before);
        prop_assert_eq!(ask_qty_sum(&book), ask_before);
    }
}
```

Adjust `OrderBook::<()>::new("TEST")` to whichever constructor form the project actually
exposes at the time the skill runs; verify with
`rg -n 'impl<.*> OrderBook' src/orderbook/book.rs`.

### 4. Invariant-specific hints

- **`trade_has_one_maker_taker`** — register a `TradeListener`, collect `TradeEvent`s into
  a `Vec`, then assert each has distinct `maker_order_id` / `taker_order_id` and that
  `trade.price == maker_resting_price` (snapshot the maker price before the fill).
- **`stp_never_self_fills`** — configure the book with one of the active STP modes, then
  filter the trade-event vec for `maker.owner == taker.owner`; assert it is empty for
  every mode under test.
- **`price_time_priority`** — assert that within each price level, the order with the
  earlier `TimestampMs` fills first. Walk the trade vec by price level and compare
  maker timestamps.
- **`replay_snapshots_match`** — run the sequencer with the in-memory journal, replay
  into a fresh book, call `snapshots_match(&live, &replayed)` and assert true. The
  sequencer's `snapshots_match` is already the canonical oracle; the proptest just widens
  coverage beyond the fixed streams in `tests/unit/`.
- **`bbo_matches_book`** — after applying the stream, compare
  `book.best_bid()` / `book.best_ask()` against the first element of
  `book.iter_levels(side)`.
- **`fees_per_fill_sum`** — configure a `FeeSchedule`, sum per-fill `fee_paid` values from
  every `TradeEvent`, compare to the `TradeResult` aggregate — assert exact equality
  (integer fee model).
- **`snapshot_restore_roundtrip`** — `let pkg = book.snapshot_package();` → build a fresh
  book → `restored.restore_from_snapshot_package(pkg)` → assert structural equality of
  price levels, cache, STP mode, fee schedule.

### 5. Config

- `cases: 256` by default. Bump to 1024+ for a nightly / release job, not for the default
  `cargo nextest run`.
- `max_shrink_iters: 50_000` — matching bugs often need aggressive shrinking to reach a
  minimal failing stream; the proptest default of 1024 is too low.
- Persist regressions: `proptest` writes failing inputs to `proptest-regressions/`. Commit
  that directory — it's the first line of defense against regressions of the same shape.

### 6. After writing

- `cargo nextest run --test props_<invariant>` (or
  `cargo test --test props_<invariant> -- --nocapture` if `nextest` is unavailable).
- If the test flakes or the shrink doesn't converge, inspect the strategy first — usually
  the price band is too wide, the owner pool too large, or the `TimeInForce` mix missing
  `PostOnly`.
- Commit with a conventional prefix: `test(orderbook): proptest for <invariant>`.

### 7. Feature gating

- Invariants that exercise `repricing.rs` (pegged / trailing-stop) must be gated:
  `#[cfg(feature = "special_orders")]` on the test function and matching CI job.
- Invariants that exercise NATS publishing should be gated on `feature = "nats"` and
  mark them `#[ignore]` by default; they are integration tests against a running server.
- Journal-replay invariants work under default features; the `journal` feature only adds
  the file-backed journal (the in-memory journal is always available).