Luna Flow
日本語

mpfr_expr_cli の設計

設計目標

1 つの MPFR 参照ファイルを単一のコマンドで frontend/mpfr_expr に通して実行します。これにより 2 進の適合性ツールは、3 つのファイル形式を知らなくても TestFloat の行列と並べて MPFR による根拠を追加できます。

数学的背景

各行は y^=∘p,ρ(f(x))\hat y = \circ_{p,\rho}(f(x))（およびフラグ）を表明します。これは mpfr_expr の設計で説明されています。ランナーは意味論に何も付け加えず、そのサマリはファイル全体に対するフロントエンドのサマリです。

設計上の判断

内容による形式の判別

各形式に共通のヘッダはないため、ランナーはマーカーを探します。初等関数の生成器は mpfr-elementary-v1 を書き出し、累乗のデータには input_coefficient_hex を含むヘッダがあり、MPFR 自身の tests/data/sqrt にはそのどちらもありません。内容に基づく判別により、固定された上流のファイルを変更せずに使えます。

シャードなし

MPFR のファイルは高々数千行です。parse_common_options は allow_shard=false で呼ばれるため、シャードオプションは黙って無視されるのではなく拒否されます。

JSON 内のコーパス名

JSON の corpus フィールドは、判別された形式と、データの生成に使われた MPFR のリリースを示します。これにより集計されたレポートは根拠の出所を明示できます。

正しさ／不変条件

  • 1 回の呼び出しで実行されるパーサはちょうど 1 つで、ファイルの内容によって決まります。
  • すべての行が成功したとき、かつそのときに限り終了コードは 0 です。totalCases = passedCases + failedCases。
  • 解析エラーの場合は、どの行も実行される前に 2 で終了します。

却下した代替案

  • --format オプション。 データにすでにあるマーカーと重複し、不一致の原因になります。
  • 複数ファイルの受け付け。 形式はファイルごとに異なります。1 プロセスにつき 1 ファイルとすることでレポートが曖昧になりません。

境界

  • シャーディングも行のフィルタリングもありません。
  • frontend/mpfr_expr の 3 つの形式のみを扱います。