レッスン8 — proptest invariant 3 個: 768 ランダムシナリオ
問い
hand-trace 9 個は思いついたシナリオを覆う。だが「limit を 17 個 submit してから空 side に market」のような、自分が思いつかない sequence のバグはどう見つけるか？ そして consensus に載せる engine の最重要 property は何か？
原理（最小モデル）
- determinism は consensus の load-bearing property。 正しいが非決定的な engine は consensus を壊す（validator が同じ action を replay して異なる約定を見て合意できない）。決定的だが間違った engine は修正可能、非決定的な engine は修復不能。
- property test が裾野を覆う + shrink。 256 case × 3 property = 768 乱数列が、hand-trace の予想外を覆う。fail した 25-action 列を最小反例まで自動 shrink する。
- 3 直交 invariant: conservation / safety / replayability。
qty_conservation（量が生まれず消えない）/no_crossed_book（常に best_bid < best_ask）/determinism（同じ入力→同じ出力）。 proptestは dev-dep、Actionenum は simplified intermediate。 test 時のみ走る（[dependencies] に入れると全 consumer に強制）。strategy は rawu64を吐き、test body がsubmit前に newtype で wrap（newtype は API 境界で効かせる）。
具体例
256 case × 3 invariant = 768 ランダムシナリオ。各 case は小さな in-memory matching simulation で、合計 10 秒未満。
失敗例（誤解）
「広い range（0..=u64::MAX）= カバレッジが多い」は誤り — 99.99% が overflow 境界（qty = u64::MAX-1）を exercise し normal な matching path を覆わない。range を plausible（account 1-200、price 50-150、qty 1-20）に絞り、予算を production traffic が exercise する path に使う。「proptest を [dependencies] に」も誤り（全 consumer に proptest コンパイルを強制）。
ここまでで「property test の役割・3 直交 invariant」は着地した。ここから組み立てる。コードは完全形。
🛑 予測。
submit_limit::Buyが時折 ask を best-first でなく random 順に辿るバグを、3 invariant のどれが最も速く / informative に catch するか？（答え:no_crossed_bookは直接（cheaper ask を残して次の bid で cross）、qty_conservationは間接、determinismは 毎回（各 run が違う「random」順を選ぶ）。determinism こそ consensus の load-bearing — なければ validator が合意できない。）
ステップで組み立てる
Step 1: crates/clob/Cargo.toml に dev-dep
[dependencies]
[dev-dependencies]
proptest = { workspace = true }
[lints]
workspace = true
proptest は既に workspace dep（consensus の proposer-election test で使用済み）。[dev-dependencies] に置けば test build 時のみ。
Step 2: mod prop_tests — Action enum + strategies
#[cfg(test)]
mod prop_tests {
use super::*;
use proptest::prelude::*;
/// A simplified action enum for property-based testing.
#[derive(Clone, Debug)]
enum Action {
SubmitLimit {
id: u64,
account: u64,
side: Side,
price: u64,
qty: u64,
},
SubmitMarket {
id: u64,
account: u64,
side: Side,
qty: u64,
},
}
fn arb_side() -> impl Strategy<Value = Side> {
prop_oneof![Just(Side::Buy), Just(Side::Sell)]
}
fn arb_action(id: u64) -> impl Strategy<Value = Action> {
let limit_action = (1u64..=200, 1u64..=20, arb_side(), 50u64..=150)
.prop_map(move |(account, qty, side, price)| Action::SubmitLimit {
id,
account,
side,
price,
qty,
});
let market_action = (1u64..=200, 1u64..=20, arb_side()).prop_map(
move |(account, qty, side)| Action::SubmitMarket {
id,
account,
side,
qty,
},
);
prop_oneof![3 => limit_action, 1 => market_action]
}
fn arb_actions() -> impl Strategy<Value = Vec<Action>> {
prop::collection::vec(0u64..1000, 1..30)
.prop_flat_map(|ids| {
ids.into_iter()
.enumerate()
.map(|(i, _)| arb_action(i as u64 + 1))
.collect::<Vec<_>>()
})
}
Action は raw u64 を持つ（newtype は test body で wrap）。arb_action の prop_oneof![3 => limit, 1 => market] で Limit を 3 倍頻度に（現実的 usage）。arb_actions の prop::collection::vec(0u64..1000, 1..30) は 長さ 1..30 を決めるためだけで、中の u64 は .enumerate() の index で上書きされる（strictly-increasing な order ID で collision 回避）。range を plausible に絞るのは、normal-looking な sequence にバグが最も隠れるから。
Step 3: 3 つの invariant（同じ proptest! block）
proptest! {
#![proptest_config(ProptestConfig {
cases: 256,
..ProptestConfig::default()
})]
/// Quantity is conserved: every fill_qty came from a resting maker;
/// total qty in/out balances.
#[test]
fn qty_conservation(actions in arb_actions()) {
let mut book = Book::new();
let mut total_in = 0u64;
let mut total_filled = 0u64;
let mut total_market_unfilled = 0u64;
for action in actions {
match action {
Action::SubmitLimit { id, account, side, price, qty } => {
total_in += qty;
let r = book.submit(Order {
id: OrderId(id),
account: AccountId(account),
side,
qty: Qty(qty),
order_type: OrderType::Limit { price: Price(price) },
});
total_filled += r.total_filled().0;
}
Action::SubmitMarket { id, account, side, qty } => {
total_in += qty;
let r = book.submit(Order {
id: OrderId(id),
account: AccountId(account),
side,
qty: Qty(qty),
order_type: OrderType::Market,
});
total_filled += r.total_filled().0;
total_market_unfilled += r.remaining_qty.0;
}
}
}
// Each fill consumes one unit from a maker AND one unit from a taker,
// so a matched unit appears in total_in twice.
let resting: u64 = book.bids.values()
.flat_map(|q| q.iter())
.chain(book.asks.values().flat_map(|q| q.iter()))
.map(|o| o.qty.0)
.sum();
prop_assert_eq!(total_in, 2 * total_filled + total_market_unfilled + resting);
}
/// Book invariant: best bid is strictly less than best ask. The book
/// should never be crossed after submit() completes.
#[test]
fn no_crossed_book(actions in arb_actions()) {
let mut book = Book::new();
for action in actions {
match action {
Action::SubmitLimit { id, account, side, price, qty } => {
book.submit(Order {
id: OrderId(id),
account: AccountId(account),
side,
qty: Qty(qty),
order_type: OrderType::Limit { price: Price(price) },
});
}
Action::SubmitMarket { id, account, side, qty } => {
book.submit(Order {
id: OrderId(id),
account: AccountId(account),
side,
qty: Qty(qty),
order_type: OrderType::Market,
});
}
}
if let (Some(b), Some(a)) = (book.best_bid(), book.best_ask()) {
prop_assert!(b < a, "book crossed: bid={} ask={}", b.0, a.0);
}
}
}
/// Determinism: applying the same action sequence produces the same
/// book + fill history every time. (Required for consensus determinism.)
#[test]
fn determinism(actions in arb_actions()) {
let run = |actions: &[Action]| {
let mut book = Book::new();
let mut all_fills: Vec<Fill> = Vec::new();
for action in actions {
let order = match action {
Action::SubmitLimit { id, account, side, price, qty } => Order {
id: OrderId(*id),
account: AccountId(*account),
side: *side,
qty: Qty(*qty),
order_type: OrderType::Limit { price: Price(*price) },
},
Action::SubmitMarket { id, account, side, qty } => Order {
id: OrderId(*id),
account: AccountId(*account),
side: *side,
qty: Qty(*qty),
order_type: OrderType::Market,
},
};
all_fills.extend(book.submit(order).fills);
}
(book.best_bid(), book.best_ask(), book.depth_bid(), book.depth_ask(), all_fills)
};
prop_assert_eq!(run(&actions), run(&actions));
}
}
}
qty_conservation: total_in = 2 × total_filled + total_market_unfilled + resting。2 × は約定が maker と taker から 1 unit ずつ消費するため（matched unit が total_in に 2 回現れる）。no_crossed_book: レッスン7 の no-cross を 256 乱数列で。determinism（最重要）: 同じ列を 2 run して 5-tuple equality。HashMap iteration / Instant::now() / tokio task / f64 bit などの non-determinism を catch — どれもコンパイルが通り no_crossed_book も pass するが、ここで catch される。#![proptest_config(cases: 256)] で各 256 回。prop_assert_eq!/prop_assert!（assert でない）が shrinking に報告。
答え合わせ
cd ~/code/openhl-reference && git checkout 55a9dff
diff -u ~/code/my-openhl/crates/clob/src/book.rs ./crates/clob/src/book.rs
git checkout main
本レッスン後、book.rs が 55a9dff を mirror（doc 以外）。Cargo.toml に [dev-dependencies] proptest。fail 入力は proptest-regressions/ に cache される（git に add）。
合格基準
cargo test -p openhl-clob
→ 12 テスト pass（unit 9 + proptest 3、各 256 case = 768 シナリオ、数秒）。よくあるミス: use proptest::prelude::*; 漏れ / total_in に約定量を足す（submit 時の order qty を足すのが正）/ determinism 失敗（HashMap や Instant 等の non-deterministic primitive 混入）。
まとめ（3行）
- proptest（256×3=768 乱数列）が hand-trace の予想外を覆い、fail 列を最小反例に shrink する。
- 3 直交 invariant: qty_conservation（保存）/ no_crossed_book（安全）/ determinism（再現性）。
- determinism が consensus の load-bearing property — 非決定的 engine は validator の合意を壊す。proptest は dev-dep に閉じる。