Inference budgets: spec vs. wired reality, and a scale/time survey
2026-06-03。サーベイノート — 参考情報であり規範ではない。仕様が拘束力を持つ。
プロジェクトがどれくらい大きくなると推論の「予算（budget）」が効き始めるのか、そしてそれは推論品質と実時間（wall time）の面でどれだけのコストを伴うのか？rigor-surveyコーパスに対して、MastodonとRedmineを大規模アプリのアンカーとして検証した。
主要な発見: 予算テーブルは配線されていない
Section titled “主要な発見: 予算テーブルは配線されていない”docs/type-specification/inference-budgets.mdは、10行からなる設定可能なbudgets:テーブル（recursion_depth、call_graph_width、operator_ambiguity、union_size、structural_growth、…）を定義している。これらのキーは現在のエンジンではいずれも読み込まれていない。 lib/全体にgrepをかけても、budgets:の設定解析も、recursion_depth / union_size / … の強制も見当たらない。このテーブルはv1向けの規範的な意図であって、現在の挙動ではない。それが参照するstatic.*の不完全推論診断ファミリーも同様に未配線である。
今日の推論を実際に制約しているのは、3つのハードコードされた、サイレントな、設定不可能な構造ガードと、1つの実在する設定可能な予算である。
| カットオフ | 場所 | 値 | 発火時 | 診断？ |
|---|---|---|---|---|
| 再帰再入ガード | ExpressionTyper#infer_user_method_return | (receiver, method)に対して深さ1 | Dynamic[top]を返す | なし（サイレント） |
| 祖先ウォーク上限 | resolve_user_def_through_ancestors | 100ノード（BFS） | 自己呼び出し解決を断念 | なし（サイレント） |
| HKTリデューサー燃料 | HktReducer#reduce | 64ステップ（ADR-20） | app.boundへ巻き戻す | なし（サイレント） |
| gemごとのソースウォーク予算 | ADR-10 dependencies.source_inference | budget_per_gem 5000（1250–20000） | カタログが切り捨てられる → Dynamic[top] | dynamic.dependency-source.budget-exceeded（唯一のもの） |
設定可能なのは最後のものだけであり、しかもそれはプロジェクトがgemをdependencies.source_inference:にオプトインしたときにのみ作動する — デフォルトはオフである。
「どの規模から予算がトリガーされるか」の再定義
Section titled “「どの規模から予算がトリガーされるか」の再定義”仕様の予算カテゴリーは構造ごと（per-construct）であって、LOCごと（per-LOC）ではない。それらはコードの形状（再帰、深い祖先チェーン、広いユニオン）に対して発火するのであって、プロジェクトの総サイズに対してではない。プロジェクトサイズは発火の頻度を変えるのであって、予算フレームワークが「起動する」閾値を変えるのではない。以下のデータがこれを裏付ける。
サーベイ1 — 規模 × 実時間（コールドなrigor check --no-cache、逐次実行）
Section titled “サーベイ1 — 規模 × 実時間（コールドなrigor check --no-cache、逐次実行）”| project | target files | wall (s) | s / file | peak RSS | diagnostics |
|---|---|---|---|---|---|
| erubi | 3 | 0.30 | 0.10 | 120 MB | 3 |
| jbuilder | 14 | 0.37 | 0.026 | 127 MB | 3 |
| haml | 51 | 1.07 | 0.021 | 126 MB | 13 |
| liquid | 64 | 0.69 | 0.011 | 129 MB | 13 |
| rubocop-ast | 99 | 0.90 | 0.009 | 128 MB | 3 |
| kramdown | 55 | 1.25 | 0.023 | 124 MB | 14 |
| redmine | 331 | 172.75 | 0.52 | 1518 MB | 723 |
| mastodon | 1219 | 173.01 | 0.14 | 277 MB | 1920 |
読み解き:
- 小さな素のRuby gemはフラットで安価である: ~0.01–0.02 s/file、~125 MBで、~100ファイルまではファイル数に関係なく一定である。
- 2つのRailsアプリは別のレジームである。 Redmineの331ファイルは、Mastodonの1219ファイルと同じ実時間を要する — Redmineは
liquidのファイルあたりコストの45倍、Mastodonは12倍である。コストはコードの形状によって支配されるのであって、ファイル数ではない。 - メモリは鋭く乖離する: Redmineは1.5 GBでピークに達するのに対し、Mastodonは4倍少ないファイル数で277 MBである。Redmineははるかに大きな推論状態を蓄積する — 広いユニオン／無制限の構造的成長のシグネチャである（まさに仕様が制限したいのにできていない
union_size/structural_growthのカテゴリー）。
サーベイ2 — 推論が実際に停止する場所（RIGOR_BUDGET_TRACE、—workers 0）
Section titled “サーベイ2 — 推論が実際に停止する場所（RIGOR_BUDGET_TRACE、—workers 0）”新しいオプトイン式カウンタ（Rigor::Inference::BudgetTrace、RIGOR_BUDGET_TRACE環境変数でゲートされ、オフのときはオーバーヘッドゼロ）が、3つのサイレントガードそれぞれを集計する。rigor checkは実行終了時にそのカウントをダンプする。
| project | recursion-guard | ancestor-walk | hkt-fuel | wall (s) |
|---|---|---|---|---|
| erubi | 0 | 0 | 0 | 0.30 |
| jbuilder | 126 | 0 | 0 | 0.37 |
| haml | 421 | 0 | 0 | 1.07 |
| liquid | 83 | 0 | 0 | 0.69 |
| rubocop-ast | 0 | 0 | 0 | 0.90 |
| kramdown | 41 | 0 | 0 | 1.25 |
| redmine | 71 | 0 | 0 | 172.75 |
| mastodon | 162 | 0 | 0 | 173.01 |
読み解き — 配線されているガードはコストの崖と直交している:
- 再帰ガードは再帰下降パーサ（haml 421、jbuilder 126、liquid 83、kramdown 41）で最も発火する — 安価なプロジェクトである。それは本物の
(receiver, method)再帰を検出してDynamic[top]を返しており、これがそれらのプロジェクトが高速に保たれる理由である: カットオフは仕事を果たしている。 - Redmine — 172 s / 1.5 GBで最も遅いプロジェクト — は再帰ガードをわずか71回しか発火させず、1秒未満の
hamlより少ない。その膨張は再帰ガードによるものではない。高価な処理は3つの配線済みガードすべてを制限なくすり抜ける。Mastodon（173 s、1219ファイル）は162回発火する — カウントはおおむねプロジェクトサイズと連動するが、ごく一部（~7.5ファイルあたり1ヒット）にとどまり、実時間とは無相関である: MastodonとRedmineはガードヒット数で2.3倍の差がありながら同じ173 sのコストである。 ancestor-walk-limitとhkt-fuelはコーパスのどこでも発火しない。100ノードの祖先上限と64ステップのHKT燃料は、今日の実コードでは負荷を担っていない。
結論: 存在する3つのガードは小さな再帰コードに対して発火しそれを高速に保つ。一方、本当の性能／メモリの崖（大規模Railsアプリ）は、まだ存在しない予算カテゴリー（union_size、call_graph_width、structural_growth）によって支配されている。それらを配線することにこそレバレッジがある — 手持ちのガードのチューニングではない。
サーベイ3 — 唯一の実在する予算: budget_per_gem（ADR-10）
Section titled “サーベイ3 — 唯一の実在する予算: budget_per_gem（ADR-10）”activesupportをdependencies.source_inference:（mode: when_missing）にオプトインした自明なプロジェクト（lib/x.rb = x = 1 + 1; puts x）を、設定可能な範囲で掃引した。解析されるファイルは付随的なもので、測定されるコストはgemのソースウォークである。
| budget_per_gem | gem_walk classes | budget-exceeded diag | wall (s) |
|---|---|---|---|
| (no source_inference) | 0 | — | 0.27 |
| 1250 (floor) | 173 | 1 | 0.30 |
| 5000 (default) | 311 | 0 | 0.33 |
| 20000 (ceiling) | 311 | 0 | 0.32 |
読み解き:
- これは実在する、観測可能な予算である。1250のフロアではウォークが切り捨てられる: activesupportの311のウォーク可能クラスのうち173しかカタログ化されず（~44%が欠落）、
dynamic.dependency-source.budget-exceededの警告が発火し、収集されなかったサーフェス（surface）への呼び出しはDynamic[top]に劣化する — 本物の品質コストである。 - 5000のデフォルトではウォークが完了し（311クラス）、上限を20000に引き上げても何も変わらない: activesupportのウォーク可能メソッド数（libルート、
Gem::Specification.find_by_name経由）は5000を下回るので、デフォルトですでにそれをカバーしている。このノブはgemの実サーフェスを超えるとプラトーに達する。 - ここでの時間への影響は小さい（0.27 → 0.33 s、311クラスで~0.05 s）。activesupportのウォーク可能サーフェスがささやかだからである。この予算の存在理由は、デフォルトのコメントが引用しているライブラリ（メソッド10,000以上のgem）であり、そこでは切り捨てがウォーク時間と診断の両方にとって重要になる。このコーパスにはそうしたオプトイン対象は存在しない。
- デフォルトオフの注意点:この予算は明示的な
dependencies.source_inference:のオプトインのもとでのみ作動する。コールドコーパスの実行（サーベイ1–2）は何もオプトインしていないため、Mastodonを含む全25コーパスプロジェクトを通じてbudget-exceededがゼロ回現れる — gemごとの予算はデフォルト実行では休眠している。 - バンドルの注意点:
find_by_nameはアクティブなバンドルからgemを解決する。BUNDLE_GEMFILE=<rigor>/Gemfile経由で実行すると、それはRigorのバンドル（activesupport 8.1.3）であって、対象アプリのものではない — したがって「Mastodonが自身のactivesupportをオプトインする」という忠実な実行にはMastodonのバンドルが必要である。ここで測定したウォークはバンドルによって決まるのであって、cwdによってではない。
サーベイ4 — ユニオンアリティ分布（Slice 2a）はunion_size仮説を反証する
Section titled “サーベイ4 — ユニオンアリティ分布（Slice 2a）はunion_size仮説を反証する”ADR-41のSlice 2aは読み取り専用のユニオンアリティ（arity）ヒストグラムを追加した: Combinator.unionが生成するすべてのType::Unionのメンバー数を、上限を強制せずに記録する（RIGOR_BUDGET_TRACE、--workers 0）。狙いは、union_sizeのデフォルトを推測ではなく観測された分布から選ぶことだった。結果はむしろunion_sizeが大規模アプリのメモリの崖に対するレバーであるという前提を反証した。
| project | union calls | max arity | p50 | p90 | p99 | ≥10 | ≥24 | ≥40 | wall | peak RSS |
|---|---|---|---|---|---|---|---|---|---|---|
| liquid | 3,514 | 20 | 2 | 3 | 4 | 4 | 0 | 0 | 0.69 s | 129 MB |
| kramdown | 9,685 | 932 | 2 | 2 | 9 | 95 | 38 | 30 | 1.25 s | 124 MB |
| haml | 15,528 | 23 | 2 | 3 | 3 | 5 | 0 | 0 | 1.07 s | 126 MB |
| redmine | 254,584 | 37 | 2 | 2 | 3 | 115 | 20 | 0 | 172.75 s | 1518 MB |
| mastodon | 873,862 | 184 | 2 | 3 | 4 | 117 | 6 | 4 | 173.01 s | 277 MB |
読み解き — 3つの発見、いずれも意思決定を変えるものである:
- メモリはユニオンの幅と相関しない — むしろ逆相関する。 kramdownは932メンバーのユニオンを生成しながら124 MB / 1.25 sでピークに達する。Redmineの最も広いユニオンは37メンバーなのに1.5 GBでピークに達する。少数の巨大ユニオンは安価であり、Redmineの膨張は広いユニオンではない。
union_sizeはRedmineにほとんど影響しないだろう。 Redmineの254,584のユニオンのうち、≥24はわずか20で、≥40はゼロである。24で制限すると20のユニオンがクリップされてメモリ上の恩恵は~0であり — しかもその20はおそらく正当なもの（Redmineの本物の分岐合流）なので、この上限は何も解決せずに偽陽性のサーフェス（topへの崩壊）を増やすだけだろう。これはまさにWD3が警告していた非対称コストの失敗であり、配線前に捕捉された。- 仕様の
union_size = 24は、どちらかといえば高すぎるのではなく低すぎる。以前の先行研究の推論（「TypeProfは10で動くので24は緩いかもしれない」）はデータによって覆される: TypeProfの10は大規模プロジェクトごとに95–117のユニオンをクリップする — Rigorの規律（discipline）のもとでは大きなFPサーフェスとなる。p99はどこでも3–9であり、唯一真に病的なテールはkramdownの932とmastodonの184である。union_sizeをそもそも配線するなら、それは~40–64の表示／病理バルブであって、メモリ修正でもなく24でもない。
帰結:負荷を担うLayer 2の問いはもはや「union_sizeを配線せよ」ではない。Redmineの1.5 GBは、プロジェクトの型ユニバースに比例して増えるがユニオンの幅とは比例しない何かによって駆動されている — 候補: structural_growth（オブジェクトシェイプ（shape）の蓄積）、ファクト（fact）ストア／ナローイングの蓄積、67k-LOCのRailsアプリのためのRBS環境、あるいは保持されたメソッドごとのスコープ。本当の次のステップは、何が実際にアロケートしているのかを見つけるためにRedmineをメモリプロファイルすることであって、ユニオン上限を配線することではない。Slice 2aはその仕事を果たした: 1回の読み取り専用測定を費やして、間違った予算を配線することを止めた。
サーベイ5 — ヒープ帰属: 崖は予算ではなくプラグインのバグだった
Section titled “サーベイ5 — ヒープ帰属: 崖は予算ではなくプラグインのバグだった”Slice 2aはunion_sizeを反証したので、Slice 2bは率直な問いを投げかけた: Redmineの1.5 GBを実際にアロケートしているのは何か？ 2つの読み取り専用プローブ（RIGOR_HEAP_PROFILE — GC後のクラス別ライブオブジェクト、RIGOR_HEAP_TRACE — アロケーションのfile:line別のライブStrings）が1回の実行でこれに答えた。
クラス内訳（Redmine、実行終了時）:追跡された756.7 MBのライブヒープのうち、671 MBがString — 4,435,826個のStringオブジェクト（89%）だった。Rigor::Type::*キャリア（carrier）はトップ30に現れなかった。型ユニバースは安価である。したがって崖は生のStringの保持であって、いかなる型レベルの構造でもない。
アロケーションサイト:それらの文字列のうち4,176,047個（98.5%）が、単一の行 — plugins/rigor-activerecord/lib/rigor/plugin/activerecord.rb:562、プラグインの@load_errorsに"… schema file not found …"を追加するrescue Errno::ENOENT — に遡った。
根本原因: schema_table_or_nilはAR呼び出しサイトごとに1回呼ばれ（model_index経由。これもnil結果をメモ化していなかった）、成功のみをメモ化していた。Redmineのスキーマファイルが欠落している（マイグレーションを同梱し、db/schema.rbがない）ため、すべての呼び出しが読み取りを再試行し、ENOENTにぶつかり、新しい補間済み文字列を追加していた。リストは際限なく成長した。これはサーベイ1の異常も説明する — Mastodonが277 MBにとどまったのはschema.rbを同梱しているためで、このバグを決してトリガーしなかった。予算という枠組みは、1つのプラグインのファイル欠落処理をスケーリング法則と取り違えていたのである。
修正＋検証:失敗をメモ化する（@schema_load_attempted、1回の試行）。Redmineを再測定した:
| metric | before | after | Δ |
|---|---|---|---|
| peak RSS | 1518 MB | 217 MB | −86 % |
| wall | 172.75 s | 84.33 s | −51 % |
| live Strings | 4,435,826 | 79,973 | −98 % |
| tracked heap | 756.7 MB | 47.6 MB | −94 % |
診断は変わらない（単一のload-error警告はすでに正しく、バグだったのは内部の保持だけである）。union_size / structural_growthの配線を動機づけた「大規模アプリのコストの崖」全体は、そもそも推論予算の問題ではまったくなかった — それは1つのプラグインにおけるメモ化されていない失敗であり、予算テーブルとは完全に直交していた。測定優先（WD3）は二重に元を取った: union_sizeを有害なデフォルトで配線することを止め、かつヒーププローブを真の原因へ一直線に導いた。
仕様デフォルトvs. 配線された現実（およびドキュメントのバグ）
Section titled “仕様デフォルトvs. 配線された現実（およびドキュメントのバグ）”仕様の予算テーブル、エンジン、ユーザー向けマニュアルは、3つの点で食い違っている:
| budget | spec default | wired value | note |
|---|---|---|---|
recursion_depth | 5 | 実効1（再入ガード） | このガードは任意の(receiver, method)の再入でDynamic[top]を返す。5レベルをアンロールすることは決してない |
ancestor_walk | （テーブルに不在） | 100 | 仕様テーブルが列挙していない、実在し負荷を担うガード |
hkt_fuel | （テーブルに不在） | 64（ADR-20） | 同様に未列挙 |
budget_per_gem | — | 5000（メソッド定義数） | マニュアルのバグ ↓ |
union_size、structural_growth、call_graph_width、overload_candidates、operator_ambiguity、interface_candidates、hash_erasure_* | 各種 | 未配線 | v1向け規範のみ |
ドキュメントのバグ: docs/manual/03-configuration.mdはdependencies.budget_per_gemを「gemごとの推論時間予算、単位ms」、デフォルト1000として記述している。どちらも誤りである: 実装された予算はメソッド定義数（catalog.sizeがそれに達するとWalkerが停止する）であり、デフォルトは5000（Dependencies::DEFAULT_BUDGET_PER_GEM）である。またbudgets:テーブルについてのユーザー向けドキュメントはそもそもまったく存在しない。修正はキューに入れた（下記のLayer 1）。
デフォルトの再検討 — 2つのレイヤー
Section titled “デフォルトの再検討 — 2つのレイヤー”「デフォルト閾値を再考する」はきれいに分割できる。なぜならサーベイは、実際に拘束力を持つ数値が、大規模アプリのコストに合わせてチューニングされた数値ではない（そのコストは予算化されていない）ことを示したからである。
Layer 1 — 安価なドキュメント／仕様の衛生（高い確信度、新たな測定不要）:
budget_per_gemのマニュアルのバグを修正する（単位＝メソッド定義数、デフォルト5000）。recursion_depthを調整する: 仕様の「5」はアンロールを含意するが、エンジンは終了保証として深さ1の再入検出を強制している（相互再帰のSystemStackErrorを止めるために追加された）。2つの意味を分離する — ハードな終了フロア（≥1）と、オプションの精度アンロール深さ（デフォルト1、すなわちオフ）と — し、仕様のデフォルトを実装された現実に合わせる。ancestor_walk（100）とhkt_fuel（64）をドキュメント化されたテーブルに追加する。どちらも実在するガードである。どちらもコーパスのどこでも発火しなかったので、値は寛大であり、そのままで構わない。operator_ambiguityを低く保つ（4）: taraiの動機は、Rigorがレシーバー型を列挙するのではなく早期に注釈を求めることを望む — FPセーフである。
Layer 2 — 結果を左右する、測定でゲートされたデフォルト:
union_size（仕様24）とstructural_growth（仕様16）は、Redmineの1.5 GBプロファイルが示唆するカテゴリーであり、未配線である。それらのデフォルトを推論で選ぶのは安全ではない: 低すぎると正当なA | B | … | 30 typesのユニオンがtopに崩壊し、メモリ上の勝利と引き換えにチェックの喪失や偽陽性を招く — 偽陽性の規律の価値への直接の違反である。決定: まずRedmine＋Mastodonで実際のユニオン／オブジェクトシェイプのサイズを計測する（ガードに使ったのと同じBudgetTraceスタイルのアプローチ — 合流アリティとシェイプメンバー成長の分布を記録する）。そのうえで、推測からではなく観測されたテールからデフォルトを選ぶ。仕様の24 / 16は、その測定が存在するまでのプレースホルダーである。- 残りの未配線の行（
call_graph_width16、overload_candidates8、interface_candidates8、hash_erasure_*）はどのコーパスプロジェクトも制約しなかった。仕様値は据え置き、あるプロジェクトがコストを実証するまで配線を延期する。
配線優先度への含意
Section titled “配線優先度への含意”union_size＋structural_growthを最初に。 Redmineの1.5 GB / ファイルあたり0.52 sのプロファイルは、無制限の合流／構造的成長をまっすぐ指し示す。これらは測定されたコストを持つカテゴリーである。他はコーパスプロジェクトが実証するまで理論上のものである。recursion_depthはすでに実質的に強制されている — 再入ガードによって深さ1で。設定可能版を配線するのは（カットオフ前に深さ>1を許容する）リファインメントであって、新しい能力ではない。ancestor_walk/ HKT燃料はハードコードのままで構わない — それらが制約するというコーパス上の証拠はない。まだそれらに設定サーフェスを費やすべきではない。- サイレントガードは、（仕様どおり）
static.*の不完全推論診断を発するべきだとおそらく言える。そうすればユーザーはDynamic[top]がどこから来たのかを見ることができる。RIGOR_BUDGET_TRACEはデバッグ用の暫定策である。それは集計のみで、単一プロセスである。
- タイミングカーブ:
nix develop→ 各プロジェクトについて、cwd＝ 対象、BUNDLE_GEMFILE=<rigor>/Gemfile bundle exec <rigor>/exe/rigor check <paths> --no-cache --format json、stats.wall_secondsを読む。 - ガードカウント: 同上、加えて
RIGOR_BUDGET_TRACE=1 --workers 0（カウンタはプロセスグローバルで、fork境界を越えない）。 - パス: Railsアプリには
app lib、それ以外にはlib（survey-initの慣習に合わせる）。
フォローアップの流れ
Section titled “フォローアップの流れ”このノートはステップ1である。何かを配線する前に（上記のLayer 1–2）:
- 比較ノート — PHPStan、TypeScript、mypy、Steep、Sorbet、TypeProfがどのように推論を制約／終了させるか（シグネチャ境界vsワイドニング付き全プログラム。それぞれが使う具体的な再帰／ユニオンサイズ／インスタンス化の制限）。
- （2）をこのサーベイと統合して、Rigorの理想的な予算設計を提案する新しいADR: どのカテゴリーを配線するか、境界契約のエスケープハッチ、測定駆動のデフォルト選択ルール。
docs/CURRENT_WORK.md § 「Inference budgets — spec table is unwired」で追跡されている。
© 2026 TypedDuck. Licensed under CC BY-SA 4.0.