Add proptest harness for the nine price-level invariants (#80)#101
Conversation
Adds proptest (dev-dependency) and a tests/proptest target (256 cases, deterministic) covering: quantity conservation, no zero-qty orders, FIFO/ price-time priority, MatchResult field agreement, Trade field invariants, IOC fill-and-discard, FOK all-or-nothing (Filled vs Killed), iceberg/reserve replenish, and snapshot round-trip + tampered-checksum. Strategies build orders through the validated newtypes and drive a single PriceLevel via match_order (post-#65 signature). Three initial counterexamples were over-strict test assumptions, not engine bugs (non-auto reserve discards stranded hidden; a replenished maker correctly loses time priority); assertions adjusted accordingly. No production code changed.
Codecov Report✅ All modified and coverable lines are covered by tests. ❌ Your project status has failed because the head coverage (73.97%) is below the target coverage (75.00%). You can increase the head coverage or adjust the target coverage. 🚀 New features to boost your workflow:
|
There was a problem hiding this comment.
Pull request overview
This PR adds a deterministic proptest-based integration test target that exercises nine single-price-level invariants against PriceLevel via the public API, improving confidence in matching correctness (FIFO, conservation, TIF behaviors, snapshot integrity) without changing production code.
Changes:
- Add
proptestas a dev-dependency and register a dedicated[[test]]target (tests/proptest/mod.rs). - Introduce shared generation strategies for makers/books/taker TIF (
tests/proptest/strategies.rs). - Implement nine property tests plus persisted regression seeds (
tests/proptest/properties.rs,tests/proptest/properties.proptest-regressions).
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| Cargo.toml | Adds proptest dev-dependency and a dedicated proptest integration test target. |
| tests/proptest/mod.rs | Wires the proptest integration test modules and documents harness behavior. |
| tests/proptest/strategies.rs | Defines proptest strategies for sides, makers, and books at a single level price. |
| tests/proptest/properties.rs | Implements the nine invariants as proptest properties over PriceLevel::match_order and snapshots. |
| tests/proptest/properties.proptest-regressions | Checks in regression seeds for CI replay of previously-found counterexamples. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
…gy fixes - prop_fifo_price_time_priority's partial-fill-keeps-front check was unreachable (required !is_complete && remaining==0). Now guarded to a STANDARD front maker with is_complete + empty filled_order_ids, so it actually exercises the invariant. Root issue: snapshot order is (timestamp, seq) while the sweep pops by seq, so random maker timestamps made "the front" ambiguous; book_strategy now stamps insertion-order-monotonic timestamps (with_id_and_ts) so the two orderings coincide. - Corrected the mod.rs doc to point at tests/proptest/properties.proptest-regressions. - Removed the stale regressions file (annotations reflected the old auto_replenish:false strategy; no engine bug, regenerated only on real failure). - book_strategy doc no longer claims "non-empty" (it honors the len range).
|
Thanks, all four addressed: the FIFO partial-fill check is now reachable and real (Standard front maker + monotonic book timestamps so snapshot/sweep ordering coincide), the regression-file doc path is corrected, the stale regressions file removed, and the book_strategy doc no longer overclaims non-empty. |
Summary
Adds a property-test harness (proptest) covering the nine named price-level
invariants, driving a single
PriceLevelthrough its public API with ordersbuilt from the validated newtypes. User-approved dev-dependency.
Changes
proptestadded to[dev-dependencies](default-features = false,features = ["std","bit-set"]); dev-only, no runtime dep.tests/proptesttarget ([[test]], 256 cases, deterministic — fixedtrade-id namespace + caller-supplied timestamps, no clock/RNG in the matcher).
strategies.rs:maker_strategy(Standard / Iceberg / auto-reserve),book_strategy,taker_tif_strategy, all via newtypes at one level price.Properties
MatchResultagreement (is_complete ⇔ remaining==0;executed_quantity == Σ trade qty;executed_value; uniquefilled_order_ids)Tradefields (maker≠taker, price==level,taker_side==maker_side.opposite())FilledvsKilledwith zero trades + untouched queue)ChecksumMismatchNotes
bugs (confirmed via the minimized cases): a non-auto reserve correctly
discards its stranded hidden when visible is consumed, and a replenished maker
correctly loses time priority (re-queued at tail). Assertions adjusted; the
generic book strategy uses
auto_replenish: true.properties.proptest-regressionsrecords those seeds so they'reretried in CI (they pass now). No production code changed.
Testing
cargo test: lib 408, proptest 9, integration 10, doctests 9 — 0 failed.cargo clippy --all-targets --all-features -- -D warnings,cargo fmt --all --check,cargo build --release: clean.Checklist
match_order(post-Decide and document taker TIF / PostOnly / MarketToLimit responsibility at the level #65)Closes #80