制御フロー解析

RigorはPHPStan、TypeScript、Pythonの型チェッカーのスタイルでフローセンシティブ（flow-sensitive）な型解析を実行します。解析器はガード、リターン、raise、ループ脱出、パターンマッチ、等価比較、述語メソッド、プラグイン提供ファクト（fact）によって型を絞り込みます。

この文書は以下を定義します:

エッジ対応スコープの構造;
サポートされているナローイング（narrowing）ソース;
ナローイングのためのRuby等価セマンティクス;
ファクトの安定性、無効化、ミューテーション効果;
出荷済みのナローイングサーフェス（surface）と、なお先送りされているもの。

RBS::Extendedアノテーションとプラグイン貢献で使われるフロー効果バンドルスキーマはrbs-extended.mdにあります。

エッジ対応スコープ

型環境はガード、リターン、raise、ループ脱出、パターンマッチ、等価比較、述語メソッド、プラグイン提供ファクトによって絞り込まれます。各式は入力Scopeで解析され、関連するエッジの出力スコープを生成します:

正常完了;
真値条件の結果;
偽値条件の結果;
例外または非リターン終了;
botで表される到達不能な結果。

これらのスコープは正のファクトと負のファクトの両方を運びます。結合はそれらのファクトを保守的にマージします。

エッジ対応スコープはif条件全体に1つのスコープを割り当てるよりも細かいです。短絡式はオペランド間でスコープを更新します:

a && bはaが生成した真値スコープでbを解析します。
a || bはaが生成した偽値スコープでbを解析します。
!aは真値スコープと偽値スコープを入れ替えます。
unless aはif aと同じ条件ファクトを使い、ブランチの宛先を入れ替えます。
case、パターンマッチ、連鎖したelsif式は、後のアームに前のアームからの負のファクトを渡します。

def contradictory(foo)
  # `foo`が有限リテラルドメインと通常のString等価を持つと仮定します。
  if foo == "foo" && foo == "bar"
    p foo # Rigorの型: bot; このエッジは到達不能です。
  end
end

&&の右辺は、左辺の真ファクトがfooを"foo"に絞り込んだ後で解析されます。その後foo == "bar"の真エッジが"foo"と"bar"の積集合を取り、botに正規化し、本体を到達不能としてマークします。Rigorは診断ポリシーに応じて比較または到達不能な本体で矛盾を報告できるべきです（SHOULD）。

||では、反対方向に同じ精度が適用されます:

def impossible_after_or(foo)
  # `foo`が有限リテラルドメインと通常のString等価を持つと仮定します。
  if foo == "foo" || foo == "bar"
    p foo # Rigorの型は"foo"と"bar"の代替のみを含みます。
  else
    p foo # Rigorの型は"foo"と"bar"の両方を除外します。
  end
end

サポートされているナローイングソース

サポートされているナローイングソースには以下が含まれます:

リテラルとシングルトン値に対する信頼された等価および不等価チェック。
nil?チェックとnil比較。
真偽性チェック（nilとfalseが偽ブランチを絞り込みます）。
is_a?、kind_of?、instance_of?、クラスとモジュールの比較。
メソッド名が静的に既知の場合のrespond_to?チェック。可視性ルールはstructural-interfaces-and-object-shapes.mdを参照してください。
パターンマッチとcase解析。
Rigorプラグインによって登録された述語メソッド。
RBS::Extendedアノテーションに記述されたアサーションとガード（rbs-extended.md参照）。

負のファクト

負のファクトはファーストクラスのスコープファクトです。Rigorは後の診断を改善する場合、「nilではない」、「falseではない」、「このリテラルではない」、「この名前的クラスを持たない」といったファクトを保持すべきです（SHOULD）。

負のファクトはドメイン相対です: 値のすでに既知の正のドメインから値を取り除きます。比較の右辺から新しい正のドメインを導入してはなりません（MUST NOT）。負のファクトの完全なセマンティクスと表示規則はtype-operators.mdにあります。

PythonのTypeGuardとTypeIsは述語効果の有用な参照点です。真ブランチのみを絞り込む述語はTypeGuardに似ています。真ブランチと偽ブランチの両方を絞り込む述語はTypeIsに似ています;内部的に偽ブランチはA & ~Rのような補完との積集合として、または同等の差分型としてモデル化すべきです（SHOULD）。

Ruby等価セマンティクス

Ruby等価はメソッドディスパッチです。foo == "foo"のような構文的比較はfoo.==("foo")を呼び出し、任意のクラスがそのメソッドをオーバーライドできます（MAY）。Rigorは以下を区別しなければなりません（MUST）:

x.equal?(obj)のような同一性ファクト（シングルトン同一性を証明できます）;
安定したRuby値テストであるnilとブーリアンチェック;
有限のString、Symbol、Integer、true、false、レシーバードメインにすでに存在するnilの代替のように、ディスパッチターゲットが安定している既知の組み込みドメインの等価ファクト;
信頼された述語と等価メソッドに対してRBSまたはプラグインが貢献した比較ファクト;
解析器が値型を絞り込むのに十分なメソッド情報を持たない限り、最大でも関係的ファクトを生成すべき（SHOULD）未知の等価メソッド;
NaN、符号付きゼロ、無限大、強制変換が完全性と等価推論を誤って述べやすくするため、デフォルトではリテラルナローイングを生成してはならない（MUST NOT）浮動小数点比較。

等価ナローイングは比較値のみから正のドメインを導入してはなりません（MUST NOT）。fooが生のuntypedであれば、foo == "foo"は、Rigorがディスパッチされた等価メソッドに信頼されたナローイング効果があることを知らない限り、動的由来の関係的ファクトを持つDynamic[top]としてfooを保持します。fooがすでに"foo" | "bar"として知られている場合、同じ比較は真ブランチを"foo"に、偽ブランチを"bar"に絞り込む場合があります（MAY）。

等価の信頼レベル

Rigorは等価ファクトを信頼レベルで分類すべきです（SHOULD）:

equal?からの同一性ファクトは、観測された参照自体が安定している限り値ファクトです。
組み込みリテラルドメイン等価は、既知のコアディスパッチターゲットを持ち、レシーバードメインがすでに互換性がある場合にのみ、すでに互換性のあるレシーバードメイン内でナローイングできます。
Module、Class、Range、Regexp、===ベースのcaseの挙動は、一般的な等価として扱うのではなく、種別ごとの明示的なルールまたはプラグインファクトが必要です。
ユーザー定義の==、eql?、===、強制変換に敏感な比較は、RBSメタデータまたはプラグインが真エッジと偽エッジの効果を宣言するまで関係的ファクトのままです。

初期の信頼された等価サーフェスは意図的に狭くなっています:

equal?は観測された参照にバインドされた同一性ファクトを生成します。このファクトは、再代入、エイリアスエスケープミューテーション、未知の呼び出し、またはプラグイン宣言効果によって無効化されます。
組み込みリテラルドメイン等価は、String、Symbol、Integer、ブーリアン、nilの有限リテラルセットに対してのみ、かつレシーバーのディスパッチターゲットが既知でレシーバードメインがすでに互換性がある場合にのみ信頼されます。
Floatリテラルナローイングはデフォルトで拒否されます。診断のために関係的ファクトを保持する場合があります（MAY）。
Range、Regexp、Module、Class、===ベースのcase挙動は、それ自体では一般的な値ナローイングファクトを生成してはなりません（MUST NOT）。値ドメインを絞り込む前に特定のナローイングルールまたはRBS/プラグイン効果が必要です。
ユーザー定義の==、eql?、===は、明示的なRBSメタデータ、RBS::Extendedフロー効果、または必要な安定性または純粋性の仮定とともにプラグイン宣言の真エッジと偽エッジのファクトを通じてのみ、関係的ファクトから値ファクトに昇格されます。

ファクトの安定性とミューテーション

フローファクトは解析器がそれらが記述するパスを信頼できる間だけ有効です。RubyのふるまいがObservedターゲットをミューテート、置換、またはエスケープさせる可能性がある場合、Rigorはファクトを無効化または弱体化させなければなりません（MUST）。

ファクトはターゲットと安定性の理由を持たなければなりません（MUST）。最初の実装では少なくとも以下を区別します:

「ローカルxは現在非nil値を参照している」のようなローカルバインディングファクト;
ブロック、proc、ラムダが別のレキシカルスコープからローカルに書き込む可能性があるキャプチャされたローカルファクト;
ハッシュキー、インスタンス変数、シングルトンメソッド、オブジェクトシェイプ（shape）メンバーのようなオブジェクトコンテンツファクト;
定数、クラス変数、グローバルのようなグローバルストレージファクト;
ローカル呼び出しを生き残る可能性があるが、それでもターゲット無効化が必要な動的由来ファクトと関係的ファクト。

ターゲット指定無効化

ローカルバインディングファクトは、そのローカルへの代入まで通常のメソッド呼び出しを越えて安定しています。呼び出しはローカルが参照するオブジェクトをミューテートする可能性がありますが（MAY）、ローカルが書き込むクロージャによってキャプチャされない限り、ローカル変数自体を再バインドしてはなりません（MUST NOT）。したがって:

x.is_a?(String)はxを書き込めない未知の呼び出しの後もローカルバインディングファクトのままです;
x[:key]またはx.fooのシェイプファクトはxをミューテートまたはエスケープさせる可能性のある呼び出しによって弱体化される場合があります（MAY）;
インスタンス変数、クラス変数、グローバル、定数に関するファクトはヒープまたはグローバルストレージファクトであり、より積極的に無効化されます。

未知のメソッド呼び出しはヒープファクトに対して保守的なままです。呼び出しにエスケープされた可能性のあるターゲットのオブジェクトシェイプ、ハッシュエントリー、インスタンス変数、定数オブジェクト、グローバルストレージファクトを無効化する場合があります（MAY）。現在のスコープのすべてのローカルバインディングファクトを無効化してはなりません（MUST NOT）。

クロージャキャプチャ

クロージャにキャプチャされたローカルには明示的な処理が必要です。ブロック、proc、またはラムダが外側のローカルに書き込む場合、Rigorはキャプチャされたローカルへの書き込み効果を記録しなければなりません（MUST）。クロージャがすぐに呼び出されてその本体が利用可能な場合、Rigorは呼び出しエッジで書き込みを適用します。クロージャがエスケープするか後で呼び出される可能性がある場合、それが書き込める可能性のあるローカルに関するファクトは、エスケープポイント以降およびそのクロージャの未知の呼び出しの前に不安定になります。

ブロック呼び出しタイミング

ブロックと高階メソッド呼び出しは、「yieldはすべてを無効化する」という一律ルールではなく、呼び出しタイミングとミューテーション効果によってモデル化すべきです（SHOULD）。有用な最初のカテゴリーは:

ブロック呼び出しなし;
即時の非エスケープ呼び出し、1回または既知の有界な回数;
即時の非エスケープ呼び出し、未知の回数;
遅延またはエスケープするブロックストレージ;
未知のブロック挙動。

tap、then、yield_self、each_with_objectのような既知のRubyメソッドは最終的にブロックタイミング、戻り値挙動、レシーバーまたは引数ミューテーションのサマリーを受け取るべきです（SHOULD）。そのようなサマリーなしでは、Rigorはオブジェクトコンテンツファクトに対して保守的である場合がありますが（MAY）、それでも無関係なローカルバインディングファクトを保持すべきです（SHOULD）。

より強いファクト保持のための証明義務

最初の実装では、より強いファクト保持のためにこれらの証明義務を使えます:

ローカルバインディングが代入されておらず、エスケープするクロージャによって書き込み可能でない;
値が不変のシングルトンまたは即値（nil、true、false、シンボル、整数など）;
値が関連操作に対してfrozenであることが証明されている;
値が新たに割り当てられ、エスケープしておらず、それをミューテートまたは格納する可能性のある呼び出しに渡されていない;
RBS、RBS::Extended、またはプラグイン効果が呼び出しがread-only、関連ターゲットに対して純粋、または特定のレシーバーまたは引数のみをミューテートすることを宣言している。

プラグインはScopeを直接ミューテートするのではなく、明示的なミューテーション、エスケープ、呼び出しタイミング、純粋性、または無効化効果を返すことができます（MAY）。バンドルスキーマはrbs-extended.mdにあります。

スコープスナップショットとファクトバケット

最初の実装ではカテゴリー分けされたファクトストアと不変のエッジごとのScopeスナップショットを組み合わせます:

各Scopeは制御フローエッジをキーとする不変スナップショットです。結合、ナローイング、無効化は、インプレースミューテーションではなく構造共有を通じて新しいスナップショットを生成します。
スナップショット内では、ファクトは上記のカテゴリーを反映したバケットに分割されます: ローカルバインディング、キャプチャされたローカル、オブジェクトコンテンツ、グローバルストレージ、動的由来、関係的。無効化ルールは特定のバケットに作用するため、未知のメソッド呼び出しはオブジェクトコンテンツをスイープしながらローカルバインディングをそのままにします。
複数のターゲットにまたがる関係的ファクトは独自のバケットに存在し、参加しているターゲットのバケットが変更を記録すると無効化されます。
Scopeの公開サーフェスはバケットを直接公開してはなりません（MUST NOT）。プラグイン、ナローイングルール、診断はターゲットに関するファクトをScopeに尋ねます;バケットレイアウトは進化する可能性がある内部最適化です（MAY）。

純粋性ポリシー

プラグイン前の純粋性ポリシーは、メソッド呼び出し結果が再呼び出しを越えて記憶されるか忘れられるかを制御します:

メソッドはデフォルトで不純として扱われます。レシーバーで不純なメソッドを呼び出すと、レシーバーのオブジェクトコンテンツバケットが無効化され、同じレシーバーへの以前の呼び出しで記憶された値ファクトが破棄されます。
純粋性は権威あるソースがそれを宣言した場合にのみ有効になります: Rigorと共に配布されるコアRubyとstdlibのRBS、受け付けられた通常のRBSファイル、またはRBS::Extendedの明示的なrigor:v1:pureアノテーション。生成されたシグネチャとプラグインの貢献はそのティア内で純粋性を絞り込む場合があります（MAY）。
設定スイッチにより、デフォルトがより「値を返すことは不純として宣言されない限り純粋」というPHPStanのポリシーに似た挙動になり、繰り返し呼び出しを越えてより強いナローイングを望むプロジェクトに対応します。スイッチはデフォルトを切り替えますが、明示的なpureまたはミューテーション宣言をオーバーライドすることはありません。
pureとレシーバーミューテーション、引数ミューテーション、またはファクト無効化効果を組み合わせることは契約（contract）の競合であり、rbs-extended.mdで指定されています。

組み込みミューテーションサマリー

最初のユーザー可視マイルストーン（v1）は、固定されたコアとstdlibクラスのセットに対して組み込みのミューテーション、純粋性、呼び出しタイミングサマリーを提供します。対象セットはArray、Hash、String、Set、IO、StringIO、File、Tempfile、Pathname、Loggerです。各サマリーは以下を記録します:

メソッドごとのレシーバーミューテーションステータス、引数ミューテーションステータス、ファクト無効化効果;
上記カテゴリーを使ったメソッドごとのブロック呼び出しタイミング;
過度の約束なしに行えるメソッドごとの純粋性宣言。

このセット外のクラスは、通常のRBS、RBS::Extended、またはプラグインファクトが別に述べるまで不純がデフォルトのポリシーに従います。Rigorはそれらの純粋性やミューテーション挙動を静かに仮定してはなりません（MUST NOT）。

先送りされたロードマップはカバレッジを追加コアクラス（Numericとその子孫、Symbol、Range、Regexp、Proc、Method、Time、Date、DateTime）、広く使われるstdlib（Date、JSON、URI、OpenStruct、Forwardable、明示的なミューテーションサマリーが必要なComparableを持つクラス）、および選択されたメタプログラミング隣接コアAPI（Module、Class、BasicObject）に拡張します。各追加は段階的に着地するため、より大きなサーフェスが着地する間も以前に出荷された挙動は乱されません。

組み込みミューテーションサマリーはクローズドリストではありません。それらを呼び出さないコードの意味を変えない限り、新しいエントリーはマイナーリリースで追加される場合があります（MAY）;公開されたロードマップは計画補助ツールであり、契約ではありません。

プラグイン前のナローイングサーフェス

プラグイン前のナローイングサーフェスは、ユーザープラグインがロードされる前に、高度にDynamic[top]なコードでRigorが生成するファクトのセットです。

この仕様は解析器が最終的にサポートする完全なプラグイン前サーフェスを記述します。最初のユーザー可視製品リリース（v1）はそのサーフェスのスコープされたスライス（slice）です;仕様を再定義するものではありません。ファクトバケット、ケイパビリティ（capability）ロールカタログ、組み込みミューテーションサマリーのような内部データ構造はv1から規範的です;ユーザーに公開される導出ルールはv1で絞られ、後続のリリースで広がります。

v1ナローイングサーフェス

nil、true、false、整数と文字列リテラル、信頼された組み込みドメインに対する等価チェックによって生成された有限リテラルユニオン（union、合併型とも）リファインメント（refinement、篩型とも）のリテラルナローイング。
構文レベルのガード: is_a?、kind_of?、instance_of?、nil?、真偽性、respond_to?、リテラルセットとの等価、および文をまたぐデータフローを必要としないcaseとcase/in形式のクラスまたはパターンマッチングナローイング。
ユーザープラグインを必要とせずにコアRubyと整理されたstdlibのサブセットにRBSまたはRBS::Extendedを使うメソッド呼び出し解決。生成されたシグネチャ（RBS::Extendedから）は参加する場合があります（MAY）。
レシーバーが静的に既知の呼び出しサイトでバンドルされたコア/stdlibミューテーションサマリーを直接適用します。サマリーはバケット無効化をローカルに駆動します。
直線コード、ブランチ結合、ループ本体を越えたナローイングファクトの手続き内伝播（0.1.xラインで出荷）。具体的な機構: 書き込み前読み取りのnil貢献、介在する / ミューテーション呼び出しによるファクト無効化、retryエッジの幅広げ、receiver[key] ||= defaultのインデックスナローイング、単一ホップのメソッドチェーンナローイング（if x.last.is_a?(Array)後のx.last）、インスタンス変数ガードナローイング（return if @ivar.nil?）。
FlowContribution経由のプラグイン提供フロー貢献 — プラグインのtruthy_facts / falsey_facts / post_return_factsがナローイングエンジンを流れる（ADR-9、v0.1.1以降）。

先送り

メソッド本体からのケイパビリティロール要件推論（カタログと明示的なconforms-toディレクティブはすでに利用可能;「本体が何のロールを必要とするか」の導出は先送り）;
プラグイン提供のフロー貢献。

各v1.1サーフェスはフィーチャーフラグの後ろで提供されるため、より大きなサーフェスが着地する間もv1の挙動は安定したままです。

診断

制御フロー解析から生まれる診断は主にflow.*ファミリーにあります。動的由来のprovenanceに依存するストリクトモードはdynamic.*ファミリーにあります。カットオフ診断はstatic.*にあります。完全な識別子分類体系はdiagnostic-policy.mdにあります。