Luna Flow
日本語

internal/conformance の設計

設計目標

4 つのコーパスフロントエンドは、まったく異なるデータ（10 進の行、区間の文、MPFR の行、TestFloat のベクトル）について結果を報告し、Python のツール群はそれらをプロセスをまたいで集計します。「ケース」「合格」「スキップ」「シャード」が何を意味するかについて一致していなければ、公表される合計は比較できなくなります。internal/conformance はその語彙を一度だけ定めます。ケースごとの処理区分、恒等式が固定されたカウンタ、そして 1 つのシャード規則です。

数学的背景

結果とカウンタ

結果は組 (id,δ,π,m)(\mathit{id}, \delta, \pi, m) であり、処理区分 δ∈{E,D,L,U}\delta \in \{\mathsf{E}, \mathsf{D}, \mathsf{L}, \mathsf{U}\}（executable、diagnostic、legacy、unsupported）、合格ビット π\pi、メッセージ mm からなります。結果のリスト RR に対し、カウンタベクトルを次のように定義します。

c(R)=∑r∈R{eexec+epassδ=E, π,eexec+efailδ=E, ¬π,eskip+eδδ∈{D,L,U},selected(R)=∣R∣,c(R) = \sum_{r \in R} \begin{cases} e_{\text{exec}} + e_{\text{pass}} & \delta = \mathsf{E},\ \pi,\\ e_{\text{exec}} + e_{\text{fail}} & \delta = \mathsf{E},\ \neg\pi,\\ e_{\text{skip}} + e_{\delta} & \delta \in \{\mathsf{D}, \mathsf{L}, \mathsf{U}\}, \end{cases} \qquad \text{selected}(R) = |R| ,

ここで ee は N7\mathbb{N}^{7} の単位ベクトルです。RunSummary::from_results は c(R)c(R) と ∣R∣|R| を正確に計算し、呼び出し側から与えられた合計 TT を格納します。

シャード

n≥1n \ge 1 と 0≤i<n0 \le i < n に対し、シャード (n,i)(n, i) は序数 Si={k∈N:k mod n=i}S_i = \{ k \in \mathbb{N} : k \bmod n = i \} を選択します。

設計上の判断

4 つの処理区分と 1 つの失敗の概念

失敗し得るのは executable の結果のみです。diagnostic、legacy、unsupported のスキップを区別することで、レポートは行が実行されなかった理由を示せます。diagnostic の行はテストではなく（失われる主張はない）、unsupported の行は欠けている機能であり（主張が失われる）、legacy の行は廃止された規約に従っています。success() は「失敗した executable のケースがない」ことを意味します。より厳格な判定は呼び出し側がその上に重ねます（ITL フロントエンドは診断でも失敗し、CLI はオプションで unsupported の行でも失敗します）。

ラウンドロビン方式のシャード

序数 kk をシャード k mod nk \bmod n に割り当てる方式は、合計を知る必要がなく、ストリーミング中に決定でき、隣接する（多くの場合コストが似た）ケースをシャード間に分散させます。検証（try_new）は使用から分離されているため、selects は 1 回の比較で済みます。

total は外部から与え、merge は最大値をとる

シャーディング前のケース数を知っているのは呼び出し側であり、シャードの結果リストではありません。1 回の実行のすべてのシャードは同じ合計 TT を報告するため、merge で最大値をとれば分割数にかかわらず TT が返りますが、総和をとると nn 回数えてしまいます。

1 始まりの位置

SourceLocation は行と列を 1 以上に切り詰めるため、整形された診断（file:line:column: message）は、「不明」を表すために 0 を渡す呼び出し側に対しても、常にエディタで有効な位置になります。

正しさ／不変条件

カウンタの恒等式。 すべてのサマリーについて、selected=executable+skipped\text{selected} = \text{executable} + \text{skipped}、executable=passed+failed\text{executable} = \text{passed} + \text{failed}、skipped=diagnostic+legacy+unsupported\text{skipped} = \text{diagnostic} + \text{legacy} + \text{unsupported} が成り立ちます。c(R)c(R) の各加数は各恒等式のちょうど一方の辺に 1 を加えるため、これらは from_results に対して成り立ちます。merge はカウンタを成分ごとに加算し、これは線形な恒等式を保存します。

シャードは序数を分割する。 すべての kk は nn を法としてちょうど 1 つの剰余を持つため、SiS_i は互いに素で N\mathbb{N} を覆います。最初の NN 個の序数のうち、シャード ii が受け取る数は

∣Si∩{0,…,N−1}∣=⌈N−in⌉,|S_i \cap \{0, \dots, N-1\}| = \left\lceil \frac{N - i}{n} \right\rceil ,

であり、したがってシャードのサイズの差は高々 1 です。

シャードを統合すると逐次実行のカウンタが得られる。 cc は、連結に関するリストから (N7,+)(\mathbb{N}^7, +) へのモノイド準同型です。c(R+ ⁣ ⁣+R′)=c(R)+c(R′)c(R \mathbin{+\!\!+} R') = c(R) + c(R') であり、同様に ∣R+ ⁣ ⁣+R′∣=∣R∣+∣R′∣|R \mathbin{+\!\!+} R'| = |R| + |R'| です。各シャードの結果が逐次実行の結果を S0,…,Sn−1S_0, \dots, S_{n-1} に制限したものであれば（ケースの結果が他のケースに依存しない限り常に成り立ちます）、

merge⁡(fr(T,R∣S0),…,fr(T,R∣Sn−1)) and fr(T,R)\operatorname{merge}\bigl(\mathrm{fr}(T, R|_{S_0}), \dots, \mathrm{fr}(T, R|_{S_{n-1}})\bigr) \text{ and } \mathrm{fr}(T, R)

はカウンタも合計も等しくなります。異なるのは結果リストの順序（シャードごとにまとめられる）だけです。

不変性。 サマリーは構築時と results() の呼び出し時に結果の配列をコピーするため、呼び出し側が後からサマリーを変更することはできません。

却下した代替案

  • 単一の「skipped」カウンタ。 テストでないものと欠けている機能の違いが隠れてしまいますが、それこそ適合性の主張が明示しなければならないものです。
  • 連続した範囲のシャード。 事前に合計が必要であり、コストの高いファイルが 1 つのシャードに集中します。
  • フロントエンドの公開 API でこれらの型を使うこと。 フロントエンドはこれらをラップするので、このパッケージは公開 API を壊さずに進化できます。

境界

  • コーパスの解析、実行、IO、JSON は扱いません。それらはフロントエンドと internal/runner_cli の役割です。
  • 時間計測や性能のデータは扱いません。
  • 結果の passed ビットがその処理区分と一致しているかは検査しません。
  • 内部用です。Luna-Flow/floating の外部からはインポートできず、安定性の約束もありません。