レッスン13 — Scanner capstone — 6 個の nuanced unit test + 4 個の invariant proptest + Liquidation三部作の振り返り
問い
これまでのテストは「skip」ケース(empty / safe / atrisk / flat)だけをカバーした。4 つの「work」outcome(solvent / fully-covered / partial-drain / depleted)と multi-account の相互作用には per-scan の assertion がまだない。型システムが encode できない不変条件(fund 会計が閉じる / unfilled⇒empty / 決定性)をどうテストし、Liquidation三部作を閉じるか?
原理(最小モデル)
- 6 個の nuanced unit test は 4×2 行列。 4 outcome(solvent / fully-covered-uw / partial-drain-uw / depleted-uw)× 2 batch shape(single / multi)。mixed-batch が 4-state 証明、FIFO が multi-underwater fairness 証明。
- 4 個の proptest が型システムで encode できない不変条件を encode。 fund 会計が閉じる(
before + deposits − withdrawals = after)/ unfilled⇒空 fund(unfilled > 0 ⇒ balance == 0)/ record 数が input 数で bound / 決定性(scan(同じ入力) ≡ scan(同じ入力))。 - 保存則が crate を縦に compose する。 3 層・3 恒等式・1 つの数学的物語:
レッスン9 (single fund call): amount + unfilled = shortfall
レッスン10 (single position close): fee_to_fund + residual_to_account = post_close_equity
レッスン13 (per-block scan batch): balance_before + Σdeposits − Σwithdrawals = balance_after
各層の保存則が次の層の invariant に consume される。crate の数学が閉じる。
- Liquidation は「計算パート・保険基金パート・スキャナパート」の 3 段構成。 計算パート(margin math)が pure-compute な分類器、保険基金パート(fund + decomposition)が state と credit/debit、スキャナパート(scanner)が両者を 1 orchestration loop で結ぶ。レッスン13 が trilogy を閉じる(69 tests、4 modules、
0a8464eに byte-for-byte 一致)。
具体例
Scan-coverage 行列:
single account multi-account
Solvent #1 ✓ (mixed でカバー)
Covered uw #2 ✓
Partial uw #3 ✓ #6 ✓ (FIFO fairness)
Depleted uw #4 ✓
Mixed-batch — #5 ✓ (4 health states)
Proptest(cross-cutting): #1 fund_balance_delta / #2 unfilled⇒empty / #3 records bound / #4 deterministic
single-account 列が 4 outcome すべてを cover、multi-account 列は interesting な複合ケース だけ(per-account 挙動は両列で同じ)。proptest は cross-cutting(全 outcome・全 batch shape に適用、直交するので行列に入らない)。
失敗例(誤解)
「4 個の proptest を 1 つの mega-property(A && B && C && D)に統合すべき」は誤り — 各 property は独立に意味を持つ。別々に証明すれば失敗メッセージが どの invariant が壊れたかを教える。mega-property の prop_assert!(A && B && C && D) は「mega-property が落ちた」とだけ言う。property レベルの粒度が失敗時の診断粒度を与える。
ここまでで「coverage 行列 + 縦に compose する保存則」は着地した。ここで Liquidation三部作を閉じる(6 unit test + 4 proptest、production コード変更なし)。コードは完全形。
🛑 予測。 1 件の liquidation が引き起こす fund state 遷移を 4 つ挙げ、どれが
Solvent入力では起こり得ないか?(答え: (a)+feeのみ(solvent — deposit、withdraw なし)/ (b)+fee_partial − shortfall(positive equity の underwater)/ (c)0 − shortfall_partial(既に underwater で fund partial drain)/ (d)0 − 0_with_unfilled(fund 空の underwater)。b/c/d は Solvent 入力では起こり得ない(レッスン10 のdebug_assert!が発火)。Solvent は (a) だけ。4 つの nuanced test が a/b/c/d を、5 つ目(mixed)と 6 つ目(FIFO)が multi-account orchestration を exercise。)
ステップで組み立てる
Step 1: 6 個の nuanced unit test
// ─── single Liquidatable: solvent close ────────────────────────
#[test]
fn scan_liquidatable_solvent_deposits_fee() {
// size=1, entry=1_000, collateral=20, mark=999.
// notional=999; fee = 999 × 150 / 10_000 = 14
// pnl = -1; post_close_equity = 19
// ratio = 19 / 999 × 10_000 = 190 bps < 200 maint → Liquidatable
// post_close_equity (19) ≥ fee (14) → solvent close
// residual_to_account = 19 - 14 = 5
let accts = vec![snapshot(7, 1, 1_000, 20)];
let mut s = LiquidationScanner::with_empty_fund(default_params());
let report = s.scan(&accts, MarkPrice(999));
assert_eq!(report.records.len(), 1);
let rec = &report.records[0];
assert_eq!(rec.account, AccountId(7));
assert_eq!(rec.classification, MarginHealth::Liquidatable);
match rec.outcome {
CloseOutcomeKind::Solvent(s) => {
assert_eq!(s.fee_to_fund, 14);
assert_eq!(s.residual_to_account, 5);
}
CloseOutcomeKind::Underwater(_) => panic!("expected Solvent"),
}
assert_eq!(report.fund_deposits, 14);
assert_eq!(report.fund_withdrawals, 0);
assert_eq!(report.unfilled_deficit, 0);
assert_eq!(s.fund_balance(), 14);
}
// ─── single Underwater: fully covered by fund ──────────────────
#[test]
fn scan_underwater_fully_covered_drains_fund_partially() {
// 1 BTC long, entry $100k, $10k collateral, mark $80,500 →
// pnl = −19_500, equity = −9_500 → Underwater.
// notional = 80_500, fee = 1_207, shortfall = 1_207 + 9_500 = 10_707.
// Start fund with $20k — covers in full.
let accts = vec![snapshot(1, 1, 100_000, 10_000)];
let fund = InsuranceFund::new(20_000);
let mut s = LiquidationScanner::new(default_params(), fund);
let report = s.scan(&accts, MarkPrice(80_500));
assert_eq!(report.records.len(), 1);
match report.records[0].outcome {
CloseOutcomeKind::Underwater(u) => {
assert_eq!(u.fee_to_fund, 0); // already underwater pre-fee
assert_eq!(u.shortfall_to_fund, 10_707);
}
CloseOutcomeKind::Solvent(_) => panic!("expected Underwater"),
}
assert_eq!(report.fund_deposits, 0);
assert_eq!(report.fund_withdrawals, 10_707);
assert_eq!(report.unfilled_deficit, 0);
assert_eq!(s.fund_balance(), 20_000 - 10_707);
}
// ─── single Underwater: fund partially drained, deficit escalates ─
#[test]
fn scan_underwater_partial_drain_surfaces_unfilled() {
// Same underwater account, but fund only has $5k — can't cover.
let accts = vec![snapshot(1, 1, 100_000, 10_000)];
let fund = InsuranceFund::new(5_000);
let mut s = LiquidationScanner::new(default_params(), fund);
let report = s.scan(&accts, MarkPrice(80_500));
assert_eq!(report.fund_withdrawals, 5_000); // drained to 0
assert_eq!(report.unfilled_deficit, 10_707 - 5_000);
assert_eq!(s.fund_balance(), 0);
}
#[test]
fn scan_underwater_depleted_fund_escalates_full_shortfall() {
// Fund empty from the start.
let accts = vec![snapshot(1, 1, 100_000, 10_000)];
let mut s = LiquidationScanner::with_empty_fund(default_params());
let report = s.scan(&accts, MarkPrice(80_500));
assert_eq!(report.fund_withdrawals, 0);
assert_eq!(report.unfilled_deficit, 10_707);
assert_eq!(s.fund_balance(), 0);
}
// ─── mixed batch ───────────────────────────────────────────────
#[test]
fn scan_mixed_batch_processes_only_unhealthy() {
// 4 accounts, all 1 long @ entry $100, mark $80 (−20% adverse).
// Vary collateral to span the 4 states:
// coll 50 → equity 30, ratio 30/80 = 37.5% → Safe
// coll 25 → equity 5, ratio 5/80 = 6.25% → AtRisk
// coll 21 → equity 1, ratio 1/80 = 1.25% → Liquidatable (solvent close)
// coll 10 → equity −10 → Underwater
let accts = vec![
snapshot(1, 1, 100, 50),
snapshot(2, 1, 100, 25),
snapshot(3, 1, 100, 21),
snapshot(4, 1, 100, 10),
];
let mut s = LiquidationScanner::new(default_params(), InsuranceFund::new(1_000));
let report = s.scan(&accts, MarkPrice(80));
assert_eq!(report.records.len(), 2);
assert_eq!(report.records[0].account, AccountId(3));
assert_eq!(report.records[1].account, AccountId(4));
assert_eq!(report.records[0].classification, MarginHealth::Liquidatable);
assert_eq!(report.records[1].classification, MarginHealth::Underwater);
}
// ─── FIFO fairness when fund partially drains ──────────────────
#[test]
fn scan_first_underwater_gets_paid_then_second_unfilled() {
// Two underwater accounts, fund has enough for the first only.
// Underwater shortfall per account: notional 80_500, fee 1_207,
// equity -9_500 → shortfall 10_707.
// Fund starts at 12_000: covers first (10_707), leaves 1_293;
// second needs 10_707 → partial 1_293 + unfilled 9_414.
let accts = vec![
snapshot(1, 1, 100_000, 10_000),
snapshot(2, 1, 100_000, 10_000),
];
let mut s = LiquidationScanner::new(default_params(), InsuranceFund::new(12_000));
let report = s.scan(&accts, MarkPrice(80_500));
assert_eq!(report.records.len(), 2);
assert_eq!(report.fund_withdrawals, 12_000); // 10_707 + 1_293
assert_eq!(report.unfilled_deficit, 10_707 - 1_293);
assert_eq!(s.fund_balance(), 0);
}
各テストの数学コメントがプリミティブから step-by-step(worked example)。#1 の境界数字(190 bps が maintenance 200 のすぐ下)が off-by-one を捕まえる。#1 の match arm 内の s は SolventClose を shadow(scope-bounded、arm 後に scanner s が戻る — だから s.fund_balance() が動く)。Perp Primer レッスン3 の数字($10,707)が #2 で 4 度目の再登場。#3 は #2 と同じ snapshot を再利用(fund サイズだけ変える、差分を isolate)。#5 mixed が 4 state を 1 呼び出しで exercise + input 順を preserve。#6 FIFO は 2 つの 同一 underwater で fairness policy を isolate、fund $12,000 = 10,707 + 1,293 ちょうど。
Step 2: 4 個の invariant proptest
// ─── proptest: invariants ──────────────────────────────────────
proptest! {
/// The scanner's `fund_balance` after a scan equals the prior
/// balance plus `fund_deposits` minus `fund_withdrawals`.
#[test]
fn fund_balance_delta_matches_report(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..10),
mark in 50_u64..150,
initial_fund in 0_i64..10_000_000,
) {
let accts: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, 100, *c))
.collect();
let mut s = LiquidationScanner::new(
default_params(),
InsuranceFund::new(initial_fund),
);
let before = s.fund_balance();
let report = s.scan(&accts, MarkPrice(mark));
let after = s.fund_balance();
// before + deposits - withdrawals = after
prop_assert_eq!(
before.saturating_add(report.fund_deposits).saturating_sub(report.fund_withdrawals),
after,
);
}
/// `unfilled_deficit > 0` implies the fund was insufficient at
/// some point during the scan, which implies `fund_balance == 0`
/// at the end of the scan.
#[test]
fn unfilled_implies_empty_fund(
collaterals in proptest::collection::vec(1_i64..1_000, 1..10),
mark in 50_u64..70, // adverse to long positions
initial_fund in 0_i64..5_000,
) {
let accts: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, 100, *c))
.collect();
let mut s = LiquidationScanner::new(
default_params(),
InsuranceFund::new(initial_fund),
);
let report = s.scan(&accts, MarkPrice(mark));
if report.unfilled_deficit > 0 {
prop_assert_eq!(s.fund_balance(), 0);
}
}
/// Number of records ≤ number of input accounts. Safe and AtRisk
/// accounts never produce records; the inequality is strict
/// when at least one input is healthy.
#[test]
fn records_count_bounded_by_accounts(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..20),
mark in 50_u64..150,
) {
let accts: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, 100, *c))
.collect();
let mut s = LiquidationScanner::with_empty_fund(default_params());
let report = s.scan(&accts, MarkPrice(mark));
prop_assert!(report.records.len() <= accts.len());
}
/// Determinism: scanning the same input twice produces the same
/// report (fresh fund + fresh scanner each time).
#[test]
fn scan_is_deterministic(
collaterals in proptest::collection::vec(1_i64..1_000_000, 0..10),
mark in 50_u64..150,
initial_fund in 0_i64..1_000_000,
) {
let accts: Vec<_> = collaterals
.iter()
.enumerate()
.map(|(i, c)| snapshot(i as u64, 1, 100, *c))
.collect();
let mut s1 = LiquidationScanner::new(
default_params(),
InsuranceFund::new(initial_fund),
);
let mut s2 = LiquidationScanner::new(
default_params(),
InsuranceFund::new(initial_fund),
);
let r1 = s1.scan(&accts, MarkPrice(mark));
let r2 = s2.scan(&accts, MarkPrice(mark));
prop_assert_eq!(r1, r2);
prop_assert_eq!(s1.fund_balance(), s2.fund_balance());
}
}
#1 fund の保存則(before + Σdeposits − Σwithdrawals = after、レッスン8 の per-call invariant を scan 全体に拡張、算術は production と一致する saturating_add/saturating_sub)。#2 fund-exhaustion 契約(unfilled > 0 ⇒ 終了時 balance == 0、入力を adverse に bias(mark 50..70、initial_fund 0..5_000)して unfilled > 0 分岐を高密度で発火 — proptest の密度問題: 広い範囲だと大多数が Safe/Solvent に着地し条件付き assertion が一度も発火せず「見えない dead-code test」になる。発火する regime に bias する)。#3 cardinality bound(<=、strict でない — 全 unhealthy なら等しい、最大 20 account)。#4 validator-consensus 契約(最も load-bearing — 同一 state の 2 scanner が byte-identical 出力、2 つ の fresh scanner、report AND fund_balance 両方を assert、ScanReport の PartialEq derive が可能にする)。
Step 3: テスト実行
cargo test -p openhl-liquidation が 69 pass(compute 34 + insurance 21 + scanner 14 = 10 unit + 4 proptest)。Liquidation crate が 0a8464e に byte-for-byte 一致、trilogy が閉じる。
答え合わせ
cd ~/code/openhl-reference && git checkout 0a8464e
diff -u ~/code/my-openhl/crates/liquidation/src/scanner.rs ./crates/liquidation/src/scanner.rs
git checkout main
scanner.rs は 0a8464e の scanner.rs と byte-for-byte 一致(doc + imports + 4 types + 5 accessor + scan + 10 unit test + 4 proptest)。他ファイルは レッスン10 以降安定。Liquidation コース完成(5 modules / 14 レッスン)。
合格基準
cargo test -p openhl-liquidation が 69 pass。よくあるエラー: scan_is_deterministic が flake(隠れた非決定性 — HashMap iterate を BTreeMap/Vec に)/ fund_balance_delta_matches_report が off-by-one(before + deposits − withdrawals の順序 — before − withdrawals への反転は中間値が負で wrap し fork)/ unfilled_implies_empty_fund が unfilled=500, balance=1000(fund depletes で early-exit している — scan を続けるべき)/ records_count_bounded_by_accounts が 21 > 20(double-push)。
設計の振り返り — Liquidation三部作
14 レッスンを通した load-bearing な決定 3 つ:
- 層を成す保存則。 レッスン9
amount + unfilled = shortfall(per call)/ レッスン10fee_to_fund + residual = post_close_equity(per close)/ レッスン13before + Σdeposits − Σwithdrawals = after(per scan)。各層の法則が次の層の invariant に consume される。最小単位から最大単位まで crate の数学が閉じる — consensus state machine を composition の下で 証明可能に 正しく保つ方法。 debug_assert!ペア + saturating arithmetic を、どこにでも。 レッスン10 dispatch は debug-assert pair、レッスン8/9 は saturating arithmetic、レッスン12 scan は両方を組み合わせる。dev-assertion + prod-saturation 規律は 1 関数から 1 crate まで scale する。- メカニズムの前に語彙、4 回連続。 レッスン1-3(types)/ レッスン8(
InsuranceFund/WithdrawOutcome)/ レッスン10(SolventClose/UnderwaterClose)/ レッスン11(scanner types)。語彙が契約を定義しメカニズムがそれを実装する。
まとめ(3行)
- 6 nuanced unit test(4 outcome の single-account + mixed-batch で 4-state + FIFO で multi-underwater fairness)+ 4 cross-cutting proptest(fund 会計 / unfilled⇒empty / record bound / 決定性)で scanner を stress テスト。69 tests で
0a8464eに一致。 - 縦に compose する保存則(per-call → per-close → per-scan)が crate の数学を閉じる。
scan_is_deterministicが最も load-bearing(consensus で非決定性 = fork)。 - Liquidation = 計算パート(pure-compute 分類器)+ 保険基金パート(state + credit/debit 分解)+ スキャナパート(orchestration loop)の 3 段構成。ADL(Layer 3)は
ScanReport.unfilled_deficitを唯一の入力に consume する別コース。
このコースの位置 / 次に来るもの
Liquidation コースは 14 レッスン・5 modules で完成(Orientation / Types / Pure compute / Insurance fund / Scanner + capstone)。safety-net cascade の Layer 1(margin 分類)+ Layer 2(insurance fund)を構築し、ADL の手前まで bridge が毎ブロック駆動できる multi-account orchestration 層を ship した。
cascade の Layer 3 — ADL(auto-deleveraging)— は別の専用コース(building-openhl-adl、openhl コミット d66b44a)。handoff は: scanner が unfilled_deficit > 0 を生む(レッスン13 proptest #2 がこれが 唯一 の signal であることを保証)→ ADL がこのフィールドを read → profitable counter-position を決定的順序で walk・force-close → insolvent ポジションに margin を credit back。レッスン13 proptest が、ADL が read する契約を固定した。