レッスン4 — Capstone — 5 invariant proptest + Liquidation〜ADL四部作の振り返り
問い
L2・L3 は hand-picked 入力で execute_adl を証明した。これを 「すべての valid 入力に対して成立する」 へどう一般化するか？ そして 4 つのコース（計算・保険基金・スキャナ・ADL）はどう 1 つの cascade に compose するのか？
原理（最小モデル）
- proptest が specific test を普遍化する。 unit test は concrete example、proptest は universal claim。両方とも必要 — 「specific が shape を、proptest が universality を証明する」。
- input strategy が「何が valid 入力か」の spec。
vec(1_i64..1_000_000, 0..15)は「0..15 候補、各 collateral 1..1M」。range は operating regime を定義する（overflow edge は L2 の saturating ops が扱う、proptest の責任ではない）。 - 5 invariant: (1) 保存則、(2) per-record decomposition、(3) aggregate accounting consistency、(4) 決定論性、(5) rank order。
具体例
保存則 proptest の核は 1 行:
prop_assert_eq!(report.deficit_absorbed + report.deficit_remaining, deficit);
L3 の Test 2・4 が 2 つの特定入力で verify したことを、デフォルト 256 ランダム入力（CI では 100,000+）で verify する。
失敗例（誤解）
「proptest があれば unit test は不要」は誤り。proptest は necessary だが sufficient ではない — 256 iteration が全 edge を hit する保証はない。疑う failure mode は L1〜3 の unit test として残す。proptest は unit test を補完するもので、置き換えるものではない。
ここまでで「proptest が何をどう普遍化するか」は着地した。ここから 5 proptest を組み立て、最後に四部作の cascade を振り返る。
🛑 予測。 Liquidation レッスン13 の capstone は 4 proptest だった。ここは 5 つ。scanner が必要としなかった 5 つ目は何か？ ヒント: ADL は record を ソート する。
（答え: records_in_rank_order。ADL のソート規律を普遍化する。scanner は record をソートしない（挿入順）。出力に構造が多いほど、preserve する invariant も多い。）
ステップで組み立てる（mod tests 末尾に proptest! ブロックを append）
proptest! {
/// Conservation: absorbed + remaining = input deficit (for
/// non-negative inputs).
#[test]
fn conservation_absorbed_plus_remaining_equals_deficit(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..15),
mark in 1_u64..1_000,
deficit in 0_i64..1_000_000,
) {
let entry = 100u64;
let candidates: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, entry, *c))
.collect();
let report = execute_adl(&candidates, MarkPrice(mark), deficit);
prop_assert_eq!(report.deficit_absorbed + report.deficit_remaining, deficit);
}
/// Every record has `pnl_paid == pnl_gross - haircut`, with
/// both haircut and pnl_paid non-negative.
#[test]
fn each_record_balances_pnl(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..15),
mark in 1_u64..1_000,
deficit in 1_i64..1_000_000,
) {
let entry = 100u64;
let candidates: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, entry, *c))
.collect();
let report = execute_adl(&candidates, MarkPrice(mark), deficit);
for rec in &report.records {
prop_assert!(rec.haircut >= 0);
prop_assert!(rec.haircut <= rec.pnl_gross);
prop_assert!(rec.pnl_paid >= 0);
prop_assert_eq!(rec.pnl_paid, rec.pnl_gross - rec.haircut);
}
}
/// Total haircuts equal `deficit_absorbed`.
#[test]
fn total_haircut_equals_deficit_absorbed(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..15),
mark in 1_u64..1_000,
deficit in 1_i64..1_000_000,
) {
let entry = 100u64;
let candidates: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, entry, *c))
.collect();
let report = execute_adl(&candidates, MarkPrice(mark), deficit);
let total: i64 = report.records.iter().map(|r| r.haircut).sum();
prop_assert_eq!(total, report.deficit_absorbed);
}
/// Determinism: same input twice → same report.
#[test]
fn execute_adl_is_deterministic(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..10),
mark in 1_u64..1_000,
deficit in 0_i64..1_000_000,
) {
let entry = 100u64;
let candidates: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, entry, *c))
.collect();
let r1 = execute_adl(&candidates, MarkPrice(mark), deficit);
let r2 = execute_adl(&candidates, MarkPrice(mark), deficit);
prop_assert_eq!(r1, r2);
}
/// Records are in non-increasing score order (or equal score
/// with strictly ascending account_id).
#[test]
fn records_in_rank_order(
collaterals in proptest::collection::vec(1_i64..1_000_000, 2..15),
mark in 100_u64..500,
deficit in 1_000_000_i64..10_000_000,
) {
// Big deficit ensures we get many records.
let entry = 100u64;
let candidates: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, entry, *c))
.collect();
let report = execute_adl(&candidates, MarkPrice(mark), deficit);
for w in report.records.windows(2) {
let (a, b) = (&w[0], &w[1]);
// Either strict score decrease, OR same score with smaller account_id first.
let ok = a.score > b.score
|| (a.score == b.score && a.account.0 < b.account.0);
prop_assert!(ok, "rank order broken between {:?} and {:?}", a, b);
}
}
}
各 proptest が何を普遍化するか
- 1. Conservation: ループ本体の
haircut + new_remaining == old_remainingが蓄積しabsorbed + remaining == deficitに。deficit in 0..が boundary(ゼロ)を含む。 - 2. Per-record decomposition: record ごと 4 sub-assertion（granular な assertion が failure を debuggable に）。0 record なら vacuously pass。
haircut <= pnl_grossが Phase 4 の.minで保証され underflow しえない。 - 3. Aggregate accounting:
∑ record.haircut == deficit_absorbed。Phase 4 が record.push と accumulator を lockstep で進める保証の cross-check（inspection より proptest が速く certain）。 - 4. Determinism: 同じ入力 2 回で full report equality。隠れた
HashMapiteration / clock read / unstable sort を catch。AdlReport: PartialEq（L1 設計）がprop_assert_eq!を可能にする。 - 5. Rank order:
.windows(2)で adjacent pair の ordering を verify。||が Phase 3 の comparator の exact 逆。deficit を 1M..10M に crank するのは、多くの record を produce して ordering を non-vacuously test するため。
答え合わせ + heavy proof
cd ~/code/openhl-reference && git checkout d66b44a
diff -u ~/code/my-openhl/crates/liquidation/src/adl.rs ./crates/liquidation/src/adl.rs
# 稀な subtle bug を炙る（CI は nightly で 100000）
PROPTEST_CASES=10000 cargo test -p openhl-liquidation adl::tests
proptest が失敗すると proptest! が自動で minimal counterexample に shrink して print する。それを通常の #[test] にコピーして deterministic に reproduce する。
Liquidation〜ADL四部作レトロスペクティブ — safety-net cascade
╔══════════════════════════════════════════════════════════════════╗
║ Per-block orchestration loop (the bridge calls this each block) ║
╠══════════════════════════════════════════════════════════════════╣
║ Layer 1 — Liquidation参照実装（計算パート）: margin classify (pure compute) ║
║ Law: phase boundaries deterministic per (snap,mark) ║
║ ↓ ║
║ Layer 1.5 — Liquidation参照実装（スキャナパート）: scanner (orchestrator) ║
║ → ScanReport { closes, unfilled_deficit } ║
║ Law: before + ∑dep − ∑wd = after (per-scan) ║
║ ↓ unfilled_deficit > 0 ║
║ Layer 2 — Liquidation参照実装（保険基金パート）: InsuranceFund (stateful) ║
║ → WithdrawOutcome (Covered/PartiallyDrained/Depleted)║
║ Law: fee + residual = equity (per-close) ║
║ ↓ != Covered ║
║ Layer 3 — ADL参照実装パート: ADL (off-orderbook fallback) ← 本コース ║
║ → AdlReport { records, absorbed, remaining } ║
║ Law: deficit_absorbed + deficit_remaining = deficit ║
║ ↓ deficit_remaining > 0 ║
║ Layer 4 — Protocol policy (out of scope) ║
║ halt the chain · accept residual · page operators ║
╚══════════════════════════════════════════════════════════════════╝
Deficit は単調に shrink: D ≥ D' ≥ D'' ≥ 0。各 layer の residual が次の入力。
構造的 takeaway が 3 つ。
- 情報フローは downstream-only — どの layer も上を読まない。各 layer の出力が次の入力を gate する。
- failure mode は最後まで typed — margin は crash しない、InsuranceFund は
WithdrawOutcomeenum で failure shape を名指す、ADL は保存則がdeficit_remainingを bound する。in-system bound を持たないのは Layer 4(protocol policy)だけ — by design。 - 各 layer に保存則があり対応コースで proptest 証明される — per-scan conservation / fee-residual decomposition /
absorbed + remaining = deficit。四部作は 4 つの別 feature ではない。同じ規律を 4 つの layer で 4 回証明したものだ。
合格基準
cargo test -p openhl-liquidation adl::tests
→ 21 テスト pass（L1 の 5 + L2 の 5 + L3 の 6 + L4 の 5 proptest）。score eligibility・pipeline correctness・保存則・decomposition・決定論性・ordering が specific 入力と random 入力の両方で証明される。コースは openhl ADL参照実装パート d66b44a に対してバイト単位で一致。DIY Perp シリーズ第 6 弾完結。
まとめ（3行）
- 5 proptest が L2/L3 の specific test を「すべての valid 入力」へ普遍化する（unit test を置き換えない）。
- input strategy の range が operating regime の spec。
records_in_rank_orderだけが ADL のソート構造ゆえに存在する。 - 四部作は 1 つの保存則規律を 4 layer で 4 回証明したもの — byte-for-byte reproducible end-to-end。