レッスン9 — withdraw_shortfall — Layer 2 → Layer 3 境界をコードで表現する
問い
fund から不足を引き出す withdraw_shortfall は、(a) balance が十分、(b) 部分的に drain して残りが出る、(c) すでに空、の 3 ケースを区別したい。戻り型は Option<i64>？ Result？ そして「型システムでは表現できない保存則（どの variant でも amount + unfilled = shortfall）」をどうテストする？
原理（最小モデル）
- 3-variant の outcome enum はカスケード境界を型で表現したもの。
Covered=「Layer 2 が完全吸収」、PartiallyDrained=「吸収できた分だけ + 残りをエスカレート」、Depleted=「Layer 2 には何もなく全部エスカレート」。ADL ルーチンがこの enum で match して何をすべきか決める。 - 全域関数のための early-return はしご。 4 ケース（非正 shortfall / 空 fund / 十分 balance / 部分 drain）をネスト
matchでなく 4 つの guarded early return で。「これは この ケースか? Yes なら return、No なら次へ」と読める。 - 保存則を proptest で encode する。 型は「3 variant ある」までは表現できるが「どの variant でも
amount + unfilled = shortfall」までは表現できない。proptest がコンパイラの enforce できない不変条件をテストスイートが enforce する 形に格上げ。 - 新 state でなく outcome を返す
&mut self。deposit（新 balance を返す）と違い、withdraw_shortfallはパスごとに質的に異なる shape を返す。mutation が質的に異なる成功モードを持つときは違いを型で返す。
具体例
3 つの variant のメンタルモデル:
balance = 1000 withdraw_shortfall(300) Covered { amount: 300 }
balance = 1000 withdraw_shortfall(1000) Covered { amount: 1000 } ← ぴったり drain
balance = 300 withdraw_shortfall(500) PartiallyDrained { amount: 300, unfilled: 200 }
balance = 0 withdraw_shortfall(500) Depleted { unfilled: 500 } ← 渡すものがない
balance = 1000 withdraw_shortfall(0) Covered { amount: 0 } ← no-op
balance = 1000 withdraw_shortfall(-100) Covered { amount: 0 } ← defensive
Covered は「ぴったり一致」と「no-op」両方を扱う（variant が意味、payload が magnitude）。Depleted は state を変えない（観測されるために存在、アクション記録のためでない）。
失敗例（誤解）
「Result<i64, FundError> にして PartiallyDrained/Depleted を error に」は誤り、問題 3 つ: (1) これらは エラーでない — エスカレート作業を surface する成功 outcome。error タグは「失敗」と「caveat 付き成功」をぼやかす。(2) ? 演算子が caller を short-circuit する（だがここでは scanning を続けたい）。(3) Result にすると全 consumer がヘルパーを Result propagation で包む。Result は「巻き戻すべきか?」、enum は「いまどんな成功をしたか?」。
ここまでで「3-variant = cascade 境界の 3 遷移」は着地した。ここから drain path を配線して insurance fund モジュールを閉じる。コードは完全形。
🛑 予測。 balance 300 に
withdraw_shortfall(500)→ 新 balance と outcome は？ 続けて同じ fund にwithdraw_shortfall(100)→ ？（答え: 1 回目 balance 0、PartiallyDrained { amount: 300, unfilled: 200 }（300 を cover、200 を ADL へ）。2 回目 balance 0 のまま、Depleted { unfilled: 100 }（呼び出し前から空なのでPartiallyDrained { amount: 0, ... }でなくDepleted）。区別は重要 —PartiallyDrained=「何か支払った」、Depleted=「何も支払っていない」、scanner は別々にログする（片方は drain しつつある、片方は枯渇した）。）
ステップで組み立てる
Step 1: withdraw_shortfall を追加
impl InsuranceFund の deposit の後に:
/// Attempt to absorb `shortfall` from the fund.
///
/// Three outcomes:
/// - `shortfall ≤ balance` → [`WithdrawOutcome::Covered`], balance
/// decreases by `shortfall`.
/// - `0 < balance < shortfall` → [`WithdrawOutcome::PartiallyDrained`],
/// balance drops to 0, unfilled = `shortfall − prior_balance`.
/// - `balance == 0` → [`WithdrawOutcome::Depleted`], no state change,
/// unfilled = `shortfall`.
///
/// Non-positive `shortfall` is treated as a successful no-op
/// (`Covered { amount: 0 }`): no balance change, no escalation.
pub fn withdraw_shortfall(&mut self, shortfall: i64) -> WithdrawOutcome {
if shortfall <= 0 {
return WithdrawOutcome::Covered { amount: 0 };
}
if self.balance == 0 {
return WithdrawOutcome::Depleted {
unfilled: shortfall,
};
}
if self.balance >= shortfall {
self.balance -= shortfall;
WithdrawOutcome::Covered { amount: shortfall }
} else {
let prior = self.balance;
self.balance = 0;
WithdrawOutcome::PartiallyDrained {
amount: prior,
unfilled: shortfall - prior,
}
}
}
early-return はしごが 4 ケースを評価順で（非正→空→十分→部分 drain、各 guard は独立、ネスト match でなくはしご）。shortfall <= 0 で負とゼロを 1 分岐（caller-facing なセマンティクスが同一）。self.balance -= shortfall は素の -（直前の guard balance >= shortfall がアンダーフロー不可を全 validator に決定論的に証明 — レッスン8 の saturating とは逆パターン、前提条件を証明できたので冗長な saturate を外す）。prior を先に保存（read→mutate→construct の時間順を明示）。&mut self + 値返し（variant 自体が成功の shape）。
Step 2: 8 個の unit test
// ─── withdraw_shortfall: Covered ───────────────────────────────
#[test]
fn withdraw_covered_typical() {
let mut f = InsuranceFund::new(1_000);
let out = f.withdraw_shortfall(300);
assert_eq!(out, WithdrawOutcome::Covered { amount: 300 });
assert_eq!(f.balance(), 700);
}
#[test]
fn withdraw_covered_exact_balance() {
let mut f = InsuranceFund::new(1_000);
let out = f.withdraw_shortfall(1_000);
assert_eq!(out, WithdrawOutcome::Covered { amount: 1_000 });
assert_eq!(f.balance(), 0);
}
#[test]
fn withdraw_zero_is_covered_noop() {
let mut f = InsuranceFund::new(1_000);
let out = f.withdraw_shortfall(0);
assert_eq!(out, WithdrawOutcome::Covered { amount: 0 });
assert_eq!(f.balance(), 1_000);
}
#[test]
fn withdraw_negative_is_covered_noop() {
// Defensive: a negative shortfall is a caller bug, not a deposit.
let mut f = InsuranceFund::new(1_000);
let out = f.withdraw_shortfall(-100);
assert_eq!(out, WithdrawOutcome::Covered { amount: 0 });
assert_eq!(f.balance(), 1_000);
}
// ─── withdraw_shortfall: PartiallyDrained ──────────────────────
#[test]
fn withdraw_partial_drains_to_zero() {
let mut f = InsuranceFund::new(300);
let out = f.withdraw_shortfall(500);
assert_eq!(
out,
WithdrawOutcome::PartiallyDrained {
amount: 300,
unfilled: 200
}
);
assert_eq!(f.balance(), 0);
}
// ─── withdraw_shortfall: Depleted ──────────────────────────────
#[test]
fn withdraw_depleted_no_change() {
let mut f = InsuranceFund::empty();
let out = f.withdraw_shortfall(500);
assert_eq!(out, WithdrawOutcome::Depleted { unfilled: 500 });
assert_eq!(f.balance(), 0);
}
#[test]
fn withdraw_after_full_drain_is_depleted() {
let mut f = InsuranceFund::new(100);
let _ = f.withdraw_shortfall(100); // Covered, drains to 0
let out = f.withdraw_shortfall(50);
assert_eq!(out, WithdrawOutcome::Depleted { unfilled: 50 });
}
// ─── deposit + withdraw sequencing ─────────────────────────────
#[test]
fn deposit_after_drain_recovers() {
let mut f = InsuranceFund::new(100);
let _ = f.withdraw_shortfall(100); // drains
f.deposit(50);
let out = f.withdraw_shortfall(30);
assert_eq!(out, WithdrawOutcome::Covered { amount: 30 });
assert_eq!(f.balance(), 20);
}
3 セクションが variant 名と一致（grep-friendly）。withdraw_covered_exact_balance は >= の境界（> への off-by-one を捕まえる）。withdraw_after_full_drain_is_depleted は state 遷移をテスト（mutation 前 balance をキャッシュする future bug を捕まえる）。deposit_after_drain_recovers は sequencing（メソッド境界を跨ぐ state-machine 遷移）。
Step 3: 4 個の proptest
mod tests 冒頭に use proptest::prelude::*;、unit test の後に:
// ─── proptest: type invariants ─────────────────────────────────
proptest! {
/// The fund's balance is never negative after any sequence of
/// deposits and withdraws.
#[test]
fn balance_never_negative(
ops in proptest::collection::vec(
proptest::prelude::any::<(bool, i64)>(),
0..20,
),
) {
let mut f = InsuranceFund::empty();
for (is_deposit, amount) in ops {
if is_deposit {
f.deposit(amount);
} else {
f.withdraw_shortfall(amount);
}
prop_assert!(f.balance() >= 0);
}
}
/// `deposit(x).deposit(y)` accumulates: balance after two deposits
/// equals the sum of the two (modulo saturation at i64::MAX).
#[test]
fn deposit_is_additive(a in 0_i64..1_000_000, b in 0_i64..1_000_000) {
let mut f = InsuranceFund::empty();
f.deposit(a);
f.deposit(b);
prop_assert_eq!(f.balance(), a + b);
}
/// After a withdraw, the change in balance equals the `amount`
/// reported in the outcome — regardless of which variant fired.
#[test]
fn withdraw_amount_matches_balance_delta(
initial in 0_i64..1_000_000,
shortfall in 0_i64..1_000_000,
) {
let mut f = InsuranceFund::new(initial);
let before = f.balance();
let out = f.withdraw_shortfall(shortfall);
let after = f.balance();
let delta = before - after;
match out {
WithdrawOutcome::Covered { amount }
| WithdrawOutcome::PartiallyDrained { amount, .. } => {
prop_assert_eq!(delta, amount);
}
WithdrawOutcome::Depleted { .. } => {
prop_assert_eq!(delta, 0);
}
}
}
/// Conservation: `amount + unfilled` across all outcome shapes
/// always equals the original (positive) shortfall.
#[test]
fn withdraw_amount_plus_unfilled_equals_shortfall(
initial in 0_i64..1_000_000,
shortfall in 1_i64..1_000_000,
) {
let mut f = InsuranceFund::new(initial);
let out = f.withdraw_shortfall(shortfall);
let total = match out {
WithdrawOutcome::Covered { amount } => amount,
WithdrawOutcome::PartiallyDrained { amount, unfilled } => amount + unfilled,
WithdrawOutcome::Depleted { unfilled } => unfilled,
};
prop_assert_eq!(total, shortfall);
}
}
balance_never_negative はレッスン8 の型不変条件そのものの proptest（任意系列で成立）。deposit_is_additive は bounded 範囲（saturation を発火させず厳密等価、境界は unit test に）。or-pattern Covered { amount } | PartiallyDrained { amount, .. }（別 variant が payload フィールドを共有）。proptest は どの variant かを予測せず property を assert（パスを assert でない）。withdraw_amount_plus_unfilled_equals_shortfall は保存則（正の shortfall のみ）。全て prop_assert!/prop_assert_eq!（shrinkage 情報）。
Step 4: テスト実行
cargo test -p openhl-liquidation が 45 pass（compute 24 + insurance 21）。insurance.rs が 260883b の withdraw まで一致。
答え合わせ
cd ~/code/openhl-reference && git checkout 260883b
diff -u ~/code/my-openhl/crates/liquidation/src/insurance.rs ./crates/liquidation/src/insurance.rs
git checkout main
insurance.rs は 260883b の insurance.rs と一致（struct/enum/3 コンストラクタ/accessor/deposit/withdraw_shortfall/Default/12 unit test/4 proptest）。lib.rs はレッスン8 以降一致。
合格基準
cargo test -p openhl-liquidation が 45 pass。よくあるエラー: balance_never_negative が [(false, -100)] で失敗（負 shortfall を deposit のように扱う — if shortfall <= 0 が最初のガード）/ withdraw_amount_plus_unfilled_equals_shortfall が total=300（PartiallyDrained が unfilled を運んでいない）/ withdraw_amount_matches_balance_delta が Depleted で delta=-N（Depleted 分岐で balance を mutate している — 触れずに return）。
まとめ（3行）
Option/Resultでなく 3-variant outcome enum — caller の決定木にマッチ（完全 absorb をログ / 部分 + escalate / depletion + escalate の 3 routing 判断）。Resultは partial-drain を失敗とタグ付けしてしまう。- 4 ケースの early-return はしご（コスト順 — 安いチェック先、構造的 mutation 最後）。
balance >= shortfallの guard を証明できたので素の-（saturate は冗長）。 - proptest が型で表現できない不変条件を encode（
balance_never_negative= 型不変条件、amount + unfilled = shortfall= 保存則）。public メソッドの契約を probe でなく prove する。
次のレッスン（レッスン10）
compute.rs に戻り、compute と insurance の橋渡しをする 3 つの pure 関数（liquidation_fee / solvent_close_outcome / underwater_close_outcome）を追加。liquidation event を (fund credit, trader 残額) or (fund debit, partial fee) に分解する — scanner が deposit/withdraw_shortfall を呼ぶのに必要な shape。