FABRKNT
Step 5. Liquidation:レバレッジ環境における非単調性の発見と清算エンジンの構築
Scanner & capstone
レッスン 14 / 14·CONTENT40 分80 XP
コース
Step 5. Liquidation:レバレッジ環境における非単調性の発見と清算エンジンの構築
レッスンの役割
CONTENT
順序
14 / 14

レッスン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 内の sSolventClose を 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..70initial_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、ScanReportPartialEq derive が可能にする)。

Step 3: テスト実行

cargo test -p openhl-liquidation69 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 は 0a8464escanner.rsbyte-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_fundunfilled=500, balance=1000(fund depletes で early-exit している — scan を続けるべき)/ records_count_bounded_by_accounts21 > 20(double-push)。

設計の振り返り — Liquidation三部作

14 レッスンを通した load-bearing な決定 3 つ:

  1. 層を成す保存則。 レッスン9 amount + unfilled = shortfall(per call)/ レッスン10 fee_to_fund + residual = post_close_equity(per close)/ レッスン13 before + Σdeposits − Σwithdrawals = after(per scan)。各層の法則が次の層の invariant に consume される。最小単位から最大単位まで crate の数学が閉じる — consensus state machine を composition の下で 証明可能に 正しく保つ方法。
  2. debug_assert! ペア + saturating arithmetic を、どこにでも。 レッスン10 dispatch は debug-assert pair、レッスン8/9 は saturating arithmetic、レッスン12 scan は両方を組み合わせる。dev-assertion + prod-saturation 規律は 1 関数から 1 crate まで scale する。
  3. メカニズムの前に語彙、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 する契約を固定した。