推論バジェットとユーザー提供の境界

Rigorは難しいケースがグローバル検索になる前に推論を停止しなければなりません（MUST）。再帰的メソッド、相互再帰呼び出しグラフ、オーバーロードされた演算子、動的ディスパッチ、大きなユニオン（union、合併型とも）、制約のない構造的推論にはすべて明示的なバジェットが必要です。バジェットが超過した場合、Rigorは精度を静かに作り出すのではなく、理由を含む不完全推論の結果を生成しなければなりません（MUST）。

この文書はバジェットカテゴリー、デフォルト、設定、ユーザー提供のカットオフの境界契約（contract）ルールを定義します。カットオフ診断はstatic.*ファミリーにあります（diagnostic-policy.md参照）。

動機となる例

演算子が多い再帰コードが動機となるケースです:

def tarai(x, y, z)
  if x <= y
    y
  else
    tarai(
      tarai(x - 1, y, z),
      tarai(y - 1, z, x),
      tarai(z - 1, x, y)
    )
  end
end

パラメータまたは戻り値契約なしでは、<=と-はすべてのRubyクラスを列挙してそれらを実装するものを一意のドメインに推論するには多態性が高すぎます。再帰呼び出しも戻り値推論をファンアウトさせます。Rigorはこの形状を早期に検出し、検索を拡大するのではなく境界を求めなければなりません（MUST）。

境界契約

受け付けられたシグネチャ契約は推論のカットオフです。#: Integerのような単純な戻り値アノテーション、完全なインライン# @rbsメソッド型、生成されたスタブ、または外部.rbs宣言はすべて、呼び出し元が宣言された戻り値を使えるようにし、メソッド境界での再帰的な戻り値推論を停止します。実装本体は契約に対して依然としてチェックされます。

この境界は深い、再帰的、または高コストのメソッドに特に価値があります。著者がすでに戻り値契約を提供しているとき、分析がメソッド本体にファンアウトするのを防ぎます。

bot戻り値契約は呼び出しが正常に返らないことを意味します。呼び出し元は到達可能性とデッドコード解析のためにbotとして扱わなければなりません（MUST）。実装解析が通常の戻り値パスを見つけた場合、Rigorはbotがインライン#: bot、# @rbs、生成されたRBS、または外部.rbsから来たかどうかに関係なく、メソッド本体に対して診断を報告しなければなりません（MUST）。

実装側のチェックは契約がどこから来たかとは無関係です。このルールを裏付けるインラインアノテーションポリシーについてはoverview.mdを参照してください。

CLIの挙動

CLIの挙動には2つのモードが必要です（MUST）:

• 非インタラクティブモードは不完全推論の診断、停止の理由、および境界契約を追加する1つ以上の互換性のある方法を報告します。
• インタラクティブモードはユーザーにrbs-inlineの戻り値#: Integer、完全なメソッドシグネチャ、または外部RBSエントリーのような境界型を求めることができます（MAY）。Rigorは明示的なユーザー確認の後にのみファイルを書き込みまたは変更しなければなりません（MUST）。

プロンプトは小さなエコシステム互換のアノテーションを優先すべきです（SHOULD）。戻り値のみの再帰カットオフには#: Integerで十分な場合があります（MAY）。レシーバーまたは演算子パラメータドメインも制約されていない場合、Rigorは(Integer x, Integer y, Integer z) -> Integerのような完全なメソッド型を求めるか、.rbsに契約を追加することを提案できます（MAY）。

境界が提供されない場合、呼び出し元は作られた精密な型を受け取ってはなりません（MUST NOT）。Rigorは内部的にDynamic[top]、top、または別の保守的な不完全推論マーカーを使える場合があります（MAY）が、診断とエクスポートは推論が停止したという事実を保持しなければなりません（MUST）。

ユーザーがdependencies.source_inference:を通じてオプトインしたGemにレシーバーが属する場合（ADR-10に従い、解析器契約: docs/internal-spec/dependency-source-inference.md）、依存関係ソース推論ティアがRBSティアより下位でDynamic[T]の回答を提供してもよく（MAY）、コールサイトを生のDynamic[top]のままにしません。このラッピングは動的由来のprovenanceを保持するため、消費者は静的ファセットTをグラウンドトゥルースの契約として頼ってはなりません（MUST NOT）——RBS / RBS::Inline / 生成されたスタブ / プラグイン契約はコンフリクト時に常に優先され、推論された形状は作成されたRBSとしてラウンドトリップされることはありません。

インタラクティブなプロンプトサーフェス（surface）はターゲット挙動であり、現在のスキャフォールド機能ではありません。非インタラクティブなカットオフパスはv1から規範的です。

バジェットテーブル

すべてのバジェットカテゴリーは.rigor.ymlのbudgets:下で設定可能であり、解析器は各エントリーに対して正常な範囲を強制しなければなりません（MUST）。受け入れられた範囲外の値は設定診断を生成し、解析器はそのキーのデフォルトにフォールバックします。

キー	カテゴリー	デフォルト	範囲
recursion_depth	再帰深度	5	1〜32
call_graph_width	呼び出しグラフ展開	16	1〜256
overload_candidates	オーバーロード候補数	8	1〜64
operator_ambiguity	呼び出しごとの演算子の曖昧さ	4	1〜32
union_size	ジョインされた戻り値のユニオンサイズ	24	4〜256
structural_growth	構造的要件の成長	16	1〜256
interface_candidates	名前付きインターフェース候補マッチ	8	1〜64
hash_erasure_keys	ハッシュシェイプ（shape）のリテラルキーユニオン	16	1〜256
hash_erasure_values	ハッシュシェイプのリテラル値ユニオン	8	1〜256
negative_fact_display	保持された否定的事実の表示	3	0〜32

hash_erasure_valuesのデフォルトは意図的にhash_erasure_keysより小さいです: ハッシュキーは値よりも識別子的な意味を持つため、より広いキーユニオンを保持することは広い値ユニオンを保持するよりも診断と消去において有用です。バジェットが消去された型をどう形成するかについてはrbs-erasure.mdを参照してください。

negative_fact_displayバジェットはtype-operators.mdに文書化された省略契約を制御します。

実装状況（2026-06-03）

上記のバジェット表はv1の規範的な意図です。本稿執筆時点で、設定可能なbudgets:サーフェス（surface）はまだ配線されていません — budgets:キーはパースされず、表の各行は強制されていません。今日エンジンが実際に適用しているカットオフは次のとおりです:

• 再帰カットオフ。設定可能なrecursion_depthではなく、(receiver, method)の再入ガード（実効的な深さ1、Dynamic[top]を返す）として動作します。
• 暗黙的selfのメソッド解決における祖先ウォーク上限（100ノード）。上記の表には載っていません。
• HKTリデューサーのfuelバジェット（64ステップ、ADR-20）。上記には載っていません。
• dependencies.budget_per_gem（ADR-10） — 唯一の設定可能なバジェットで、dependencies.source_inference:によるオプトインです。

残りの行 — コストを担うunion_sizeとstructural_growthを含む — はまだ強制されていません。ターゲットとなる設計、配線計画（Layer 1のドキュメント/仕様の衛生、Layer 2の計測ゲート付き配線）、およびヒット時のstatic.*診断ポリシーはADR-41に記録されています。裏付けとなる調査はdocs/notes/20260603-inference-budget-reality-survey.mdです。RIGOR_BUDGET_TRACEは配線済みの3つのガードについて実行ごとのカウントを公開します。

カットオフカテゴリー

初期のバジェットカテゴリーはカットオフが予測可能になるように明示的です:

• 同じメソッドまたは相互再帰クラスタに対する再帰深度。
• 本体が契約なしで多くの呼び出し先にファンアウトするときの呼び出しグラフ展開幅。
• 引数感度ディスパッチに対するオーバーロード候補数。
• <=や-のような演算子が多くのレシーバー型を受け付けるときの呼び出しごとの演算子の曖昧さ。
• ジョインされた推論戻り値のユニオンサイズ。
• ケイパビリティ（capability）サマリーが新しいメンバーを取得し続けるときの構造的要件の成長。
• ロール推論が名前付きインターフェースのマッチを探すときに使われる名前付きインターフェース候補マッチ（structural-interfaces-and-object-shapes.md参照）。

各バジェットは作られた精密な型ではなく、理由を含む不完全推論の結果を生成します。これにより推論は「Rubyコードに特定のRigorインラインシグネチャ構文なし」という目標と互換性が保たれます: ユーザーはRigorのみのDSLではなく、受け付けられたRBS形状の契約でカットオフを解決します。