レッスン5 — account_equity + margin_ratio — そして最初のメンタルモデルを壊す proptest

問い

「long ポジションで mark が上がれば margin_ratio も上がる」— これは直感的に正しそうだ。proptest でこの不変量を主張したら、通るか？ もし小さな入力で失敗したら、それは関数のバグか、それとも不変量の書き方のバグか？

原理（最小モデル）

• account_equity は i64、負にもなりうる。 collateral + unrealized_pnl で PnL が collateral を突き抜けて不足を生む。エンジンは不足を 測れる 必要がある（でないと正しいレバーを引けない）。
• margin_ratio は notional == 0 を MarginRatio(i64::MAX) でガード。 flat は exposure ゼロ → margin 要件なし。最大 ratio = 「無限に safe」で、下流分類器が special-case なしに short-circuit できる。
• equity × MARGIN_SCALE / notional の演算順。 先に i128 で掛ければ小さい ratio も割り算を生き残る。先に i64 で割ると精度が落ちる。
• levered regime での非単調性。 「mark↑ → ratio↑」は collateral > entry × size の cash-heavy regime では 成り立たない。proptest が捕まえる。対処は関数のパッチでなく、不変量の表現の refine。
• prop_assume! が条件付き不変量を書く道具。 不変量が入力空間の一部でしか成り立たないとき、assertion を弱めず入力をそのサブセットにフィルタする。
• short と long で monotonicity の対称性が崩れる。 short は mark に対して 無条件に monotonic、long はレバレッジが効く条件下でのみ。微分が理由を説明する。

具体例

long で collateral = 103、size = 1、entry = 100 のとき:

mark = 1:  notional=1,  pnl=(1−100)×1=−99, equity=103−99=4, ratio=4×10_000/1   = 40_000 bps (400%)
mark = 2:  notional=2,  pnl=(2−100)×1=−98, equity=103−98=5, ratio=5×10_000/2   = 25_000 bps (250%)

mark が上がったのに ratio は 400%→250% に 下がった。equity も上がった（4→5）が notional も上がり（1→2）、notional のほうが速く成長した。collateral > entry × size の cash-heavy regime では、mark が動くと ratio はどちらにも動きうる。

失敗例（誤解）

「long-monotonicity proptest が失敗したら margin_ratio にバグがあるので関数を直す」は誤り — 関数は正しい。バグは proptest の不変量の書き方にある（monotonicity が成り立たない regime に対しても主張している）。微分 d(ratio)/d(mark) = MARGIN_SCALE/mark² × (entry − collateral/size) の符号は entry × size と collateral の大小で決まる。対処は prop_assume! で levered regime に絞ること。

ここまでで「ratio は levered regime でのみ mark に monotonic」は着地した。ここから「書く→失敗→トレース→refine」の proptest discovery loop を実演する（これが本レッスンの load-bearing なスキル、急がない）。コードは完全形。

🛑 予測。 long で collateral=100, size=1, entry=100 のとき、mark=100/110/50 での margin_ratio は？（答え: 全部 10_000 bps = 100%。collateral がちょうど notional_at_entry に等しく、どの mark でも PnL の動きを collateral が相殺する。unlevered（exposure $1 に collateral $1）。ここが素朴な monotonicity の直感が壊れる regime — collateral ≥ notional_at_entry の cash-funded position では mark が動くと ratio はどちらにも動く。）

ステップで組み立てる

Step 1: account_equity を追記

/// Account equity = `collateral + unrealized_pnl`. Can be negative.
///
/// A negative equity means losses have exceeded deposited collateral —
/// the account is underwater. The liquidation engine still attempts to
/// close the position; any residual deficit falls to the insurance fund.
#[must_use]
pub fn account_equity(snapshot: &AccountSnapshot, mark: MarkPrice) -> i64 {
    snapshot
        .collateral
        .0
        .saturating_add(unrealized_pnl(snapshot, mark))
}

返り型 i64（doc が「負になりうる」、型がそれを本物に）。saturating_add（+ でも checked_add でもない — 極端値で i64::MAX/MIN を返し、どちらも明確な health state として分類できる）。

Step 2: margin_ratio を追記

/// Margin ratio = `equity / notional`, scaled by [`MARGIN_SCALE`].
///
/// Returns `MarginRatio(i64::MAX)` for a flat position — no notional
/// exposure means the margin requirement is irrelevant, and we report the
/// healthiest possible ratio.
///
/// Returns a negative ratio when equity < 0 (the underwater case).
#[must_use]
pub fn margin_ratio(snapshot: &AccountSnapshot, mark: MarkPrice) -> MarginRatio {
    let notional = notional_value(snapshot, mark);
    if notional == 0 {
        return MarginRatio(i64::MAX);
    }
    let equity = account_equity(snapshot, mark);
    // ratio = equity × MARGIN_SCALE / notional, in i128 to avoid overflow
    // before the divide.
    let scaled = i128::from(equity).saturating_mul(i128::from(MARGIN_SCALE));
    let ratio = scaled / i128::from(notional);
    MarginRatio(saturate_i128_to_i64(ratio))
}

notional == 0 で i64::MAX（flat = 無限に safe、下流の if ratio >= initial_bps { Safe } が特例分岐なしに通る magic boundary）。乗算を除算より先に（小さい ratio も割り算を生き残る）。scaled product を i128 で受ける。整数のゼロ除算は panic するのでガード必須。

Step 3: unit test を 5 個追加

    // ─── account_equity ────────────────────────────────────────────

    #[test]
    fn equity_collateral_plus_pnl() {
        // Long 10 @ 100, collateral 1_000, mark 120 → equity = 1_000 + 200 = 1_200
        let s = snapshot(10, 100, 1_000);
        assert_eq!(account_equity(&s, MarkPrice(120)), 1_200);
    }

    #[test]
    fn equity_can_go_negative() {
        // Long 10 @ 100, collateral 100, mark 50 → pnl = −500, equity = −400
        let s = snapshot(10, 100, 100);
        assert_eq!(account_equity(&s, MarkPrice(50)), -400);
    }

    // ─── margin_ratio ──────────────────────────────────────────────

    #[test]
    fn ratio_flat_returns_max() {
        let s = snapshot(0, 100, 1_000);
        assert_eq!(margin_ratio(&s, MarkPrice(100)), MarginRatio(i64::MAX));
    }

    #[test]
    fn ratio_exactly_ten_percent() {
        // Notional = 10 × 100 = 1_000; equity = 100 (collateral only, pnl = 0).
        // ratio = 100 × 10_000 / 1_000 = 1_000 bps = 10%.
        let s = snapshot(10, 100, 100);
        assert_eq!(margin_ratio(&s, MarkPrice(100)), MarginRatio(1_000));
    }

    #[test]
    fn ratio_can_be_negative() {
        // Underwater: equity = −400, notional = 500 → ratio = −8_000 bps
        let s = snapshot(10, 100, 100);
        let r = margin_ratio(&s, MarkPrice(50));
        assert!(r.0 < 0, "expected negative ratio, got {:?}", r);
    }

各 ratio テストがコメントで厳密な算術を名指し。ratio_can_be_negative は assert!(r.0 < 0)（厳密値でなく符号 — rounding artifact をロックしない、property をテスト）。

Step 4: Proptest を書く — 素朴な初版（prop_assume! なし）

    proptest! {
        /// For a long position, as mark increases (price moves in the
        /// long's favor), margin_ratio should monotonically increase.
        /// If it ever moved the other way, an account could pass from
        /// "safe" to "liquidatable" without a single adverse price move,
        /// which would be a soundness bug.
        #[test]
        fn long_ratio_monotonic_in_mark(
            size in 1_i64..1_000,
            entry in 100_u64..10_000,
            collateral in 1_i64..1_000_000,
            mark_a in 1_u64..50_000,
            mark_b in 1_u64..50_000,
        ) {
            prop_assume!(mark_a < mark_b);
            let s = snapshot(size, entry, collateral);
            let r_low  = margin_ratio(&s, MarkPrice(mark_a));
            let r_high = margin_ratio(&s, MarkPrice(mark_b));
            prop_assert!(
                r_low.0 <= r_high.0,
                "long ratio not monotonic: mark_a={} → r={}; mark_b={} → r={}",
                mark_a, r_low.0, mark_b, r_high.0
            );
        }
    }

cargo test すると最小 counterexample で 失敗: mark_a=1 → r=40000; mark_b=2 → r=25000（minimal: size=1, entry=100, collateral=103）。ここで止まる。関数を直さない。失敗を手でトレースする。

Step 5: 失敗を手で辿る

mark=1: notional=1, pnl=−99, equity=4, ratio=40_000 bps。mark=2: notional=2, pnl=−98, equity=5, ratio=25_000 bps。mark が上がると ratio が下がった（equity も上がったが notional がより速く成長）。一般式 ratio = MARGIN_SCALE × (collateral/notional + (1 − entry/mark)) を mark で微分:

d(margin_ratio)/d(mark) = MARGIN_SCALE / mark² × (entry − collateral / size)

符号は entry − collateral/size の符号と一致:

                         margin_ratio (Long、collateral と size を固定して mark を動かす)
   🔴 Cash-heavy (collateral > entry × size): ratio は mark↑ で ↘ 減少 ← 素朴な直感が破綻
   ◆ 境界 (collateral = entry × size, ちょうど 1x): ratio は mark に水平 (微分 = 0)
   🟢 Levered  (collateral < entry × size): ratio は mark↑ で ↗ 増加 ← 直感どおり、現実の 99%

境界の位置は collateral と entry × size の大小だけで決まる（mark に依存しない）。失敗入力は entry×size=100, collateral=103 で collateral > entry×size の cash-heavy regime。これは margin_ratio のバグではない。関数は正しい。バグは proptest が monotonicity の成り立たない regime にも monotonicity を主張していること。

Step 6: prop_assume! で refine

    proptest! {
        /// For a *levered* long position (entry × size > collateral), as
        /// mark increases, margin_ratio monotonically increases.
        ///
        /// The leverage condition is load-bearing: when collateral exceeds
        /// position notional at entry (effectively cash + tiny exposure),
        /// the ratio is dominated by `collateral / notional`, which
        /// *decreases* as mark grows — so monotonicity fails. That
        /// regime is uninteresting for liquidation (the account can
        /// never be liquidated), so we exclude it via `prop_assume!`.
        #[test]
        fn long_ratio_monotonic_in_mark_when_levered(
            size in 1_i64..1_000,
            entry in 100_u64..10_000,
            collateral in 1_i64..1_000_000,
            mark_a in 1_u64..50_000,
            mark_b in 1_u64..50_000,
        ) {
            prop_assume!(mark_a < mark_b);
            // Levered regime: notional at entry strictly exceeds collateral.
            prop_assume!(
                i128::from(entry) * i128::from(size) > i128::from(collateral)
            );
            let s = snapshot(size, entry, collateral);
            let r_low  = margin_ratio(&s, MarkPrice(mark_a));
            let r_high = margin_ratio(&s, MarkPrice(mark_b));
            prop_assert!(
                r_low.0 <= r_high.0,
                "long ratio not monotonic: mark_a={} → r={}; mark_b={} → r={}",
                mark_a, r_low.0, mark_b, r_high.0
            );
        }

テスト名末尾が _when_levered（名前が前提条件を運ぶ）。doc が前提条件の なぜ を名指し（意図的 scope 選択であって見落としでない）。入力レンジを制限せず prop_assume! を使う（inter-parameter 制約は strategy で組みにくい、assume なら assertion の隣で読める）。

Step 7: Short-monotonicity proptest を追加（前提条件なし）

        /// Symmetric invariant for shorts: as mark increases, the short's
        /// margin_ratio always decreases. Unlike the long case, this holds
        /// for *any* collateral level — the math derivative is uniformly
        /// negative in mark (every term either decreases or stays flat).
        #[test]
        fn short_ratio_monotonic_in_mark(
            size in 1_i64..1_000,
            entry in 100_u64..10_000,
            collateral in 1_i64..1_000_000,
            mark_a in 1_u64..50_000,
            mark_b in 1_u64..50_000,
        ) {
            prop_assume!(mark_a < mark_b);
            let s = snapshot(-size, entry, collateral);
            let r_low  = margin_ratio(&s, MarkPrice(mark_a));
            let r_high = margin_ratio(&s, MarkPrice(mark_b));
            prop_assert!(
                r_low.0 >= r_high.0,
                "short ratio not monotonic: mark_a={} → r={}; mark_b={} → r={}",
                mark_a, r_low.0, mark_b, r_high.0
            );
        }

leverage 条件の prop_assume! がない（short monotonicity は無条件 — size<0 で微分 = MARGIN_SCALE/mark² × (−collateral/|size| − entry) の両項が非正、一様に負）。この非対称性は本物の数学的事実。snapshot 構築時に -size を渡す（generator には正の size、size=0 の flat を避ける）。

Step 8: Determinism proptest を追加

        /// Determinism: the same inputs always produce the same MarginRatio.
        /// Trivially true for pure functions, but the proptest catches
        /// accidental non-determinism (e.g., if a future refactor introduces
        /// HashMap iteration or float arithmetic).
        #[test]
        fn margin_ratio_deterministic(
            size in -1_000_i64..1_000,
            entry in 1_u64..10_000,
            collateral in -1_000_000_i64..1_000_000,
            mark in 1_u64..50_000,
        ) {
            let s = snapshot(size, entry, collateral);
            let r1 = margin_ratio(&s, MarkPrice(mark));
            let r2 = margin_ratio(&s, MarkPrice(mark));
            prop_assert_eq!(r1, r2);
        }
    }

pure 関数には自明だが 将来 のリグレッション（HashMap iteration / SystemTime / float の誤混入）を chain fork 前に捕まえる。広い入力レンジ（determinism はどこでも成り立つ）。維持コスト最小・違反発見コスト最小。

Step 9: lib.rs を更新

pub use compute::{account_equity, margin_ratio, notional_value, unrealized_pnl};

Step 10: テスト実行

cargo test -p openhl-liquidation が 16 pass（unit 13 + proptest 3、各 256 ケース ≈ 768 入力）。successes: 220, rejects: 36 のような出力は問題なし（prop_assume! フィルタ）。

答え合わせ

cd ~/code/openhl-reference && git checkout 22eedf9
diff -u ~/code/my-openhl/crates/liquidation/src/compute.rs ./crates/liquidation/src/compute.rs
diff -u ~/code/my-openhl/crates/liquidation/src/lib.rs ./crates/liquidation/src/lib.rs
git checkout main

compute.rs は margin_ratio + 最初の 13 unit test + 3 proptest まで一致（margin_health/close_order_spec は L6/L7）。lib.rs は compute re-export 6 個中 4 個。

合格基準

cargo test -p openhl-liquidation が 16 pass。サプライズ: successes: 220, rejects: 36 は正常（assume フィルタ）/ proptest が想定より時間かかる場合も pure 算術なので実用上十分速い。

まとめ（3行）

• account_equity: i64（負になりうる、underwater を測れる）/ margin_ratio は flat を MarginRatio(i64::MAX) でガード（「制約なし」を「最も safe な値」で表現、下流が special-case なしに short-circuit）。
• proptest の失敗そのものがレッスン — 素朴な long-monotonicity が cash-heavy regime（collateral > entry×size）で破れる。微分を自分で歩いて「ratio は levered regime でのみ monotonic」に到達。
• 条件付き不変量には prop_assume!（関数を強めず assertion を弱めず strategy を手で制限せず）。short は無条件 monotonic、long は levered のみ — この非対称は本物の数学的事実。

次のレッスン（レッスン6）

margin_health を追加（MarginRatio を params と比較し 4 variant にマップ）。境界 unit test 5 個と、各しきい値で strict-less-than を使う理由、最も極端な state を最初に check する cascade 順を見る。