frontend/mpfr_expr の設計

設計目標

GNU MPFR は、任意の精度、すべての丸め方向で、初等関数の正しく丸められた結果を計算します。¹1 L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, P. Zimmermann, “MPFR: A multiple-precision binary floating-point library with correct rounding”, ACM TOMS 33(2), 2007. このパッケージは MPFR の出力を bin_float 向けの実行可能な検査に変換します。行が合格することは、その入力・精度・丸めモードについて bin_float が正しく丸められた結果（および正しい例外フラグ）を返すことを示します。これは純粋なライブラリであり、データファイルとその来歴は testdata/bin_float/ に、生成器は tools/ にあります。

数学的背景

正しい丸め

$\mathbb{F}_p$ を $p$ ビットの仮数部と非有界な指数を持つ 2 進数の集合とし、 $\circ_{p,\rho}$ を方向 $\rho$ での $\mathbb{F}_p$ への丸めとします。実関数 $f$ と $x \in \mathbb{F}_q$ に対し、正しく丸められた結果は次のとおりです。

y = \circ_{p,\rho}\bigl(f(x)\bigr), \qquad \text{inexact} \iff f(x) \notin \mathbb{F}_p .

MPFR は $y$ と、 $y$ が $f(x)$ より小さいか、等しいか、大きいかを符号で示す三値（ternary value）を返します。生成器はこれを inexact フィールドに変換します。特殊な点では IEEE 754 の規則が適用されます。無効演算（たとえば $\sqrt{-1}$ 、 $\ln(-1)$ ）は invalid フラグとともに NaN を返し、有限のオペランドからの正確な無限大の結果（ $\ln 0 = -\infty$ ）はゼロ除算を発生させます。²2 IEEE 754-2019 の第 7.2 節（無効演算）と第 7.3 節（ゼロ除算）、および推奨される初等関数については第 9.2 節。

行が主張する内容

各形式は $f$ 、入力 $x$ 、目標精度 $p$ 、方向 $\rho$ を固定し、MPFR の $y$ （およびフラグ）を記録します。実行器は対応する bin_float メソッドを BinaryContext::unbounded(p, rounding=ρ) で評価し、次を検査します。

形式	値の検査	フラグの検査
平方根	`BinFloat` 値として $\hat y = y$ （`==`）	なし
整数べき $x^n$	$\hat y = y$ (`==`)	inexact が等しい。underflow、overflow、division by zero、invalid はなし
初等関数	$\hat y \simeq y$ (`compare == 0`)	inexact、invalid、division by zero が等しい。underflow、overflow はなし

BinFloat に対する == は格納された表現を比較します。この表現は与えられた値と精度に対して正準なので、 $+0$ と $-0$ 、および NaN のペイロードを区別します。compare == 0 は数値的な等価性を拡張したもので、すべての NaN はすべての NaN と等しく、 $+0 = -0$ となります。

設計上の判断

非有界な指数範囲

MPFR の既定の指数範囲はどの IEEE 形式よりもはるかに広く、データには非正規化数の範囲にある binary64 入力から計算された $2^{-563}$ のような結果が含まれます。非有界なコンテキストで実行することで、仮数部の丸めを単独でテストします。範囲に起因する効果（オーバーフロー、アンダーフロー、非正規化数）は、形式に実際の限界がある testfloat_expr を通じて TestFloat コーパスがカバーします。したがって、MPFR の行でアンダーフローまたはオーバーフローのフラグが立つことは不合格です。それは欠陥からしか生じ得ません。

入力は 512 ビットで読み取る

入力は 16 進数で書かれており、正確な 2 進数です。初等関数とべき乗の入力を 512 ビットで読み取ると、有効ビット数が 512 以下のすべての入力が正確に保たれるため、検査の対象は $x$ の解析ではなく $f$ になります。平方根の形式は独自の入力精度を持ち、その精度で読み取られます。

初等関数の行は数値的に比較する

初等関数のマトリクスは、29 個の関数について binary32/64/128 の精度と 6 つの丸めモードすべてにわたって生成されます。期待される NaN はペイロード情報を持たず、IEEE 754 は生成される NaN のペイロードを実装に委ねているため、比較ではすべての NaN を等しいものとして扱います。同じ数値比較では $+0$ と $-0$ も同一視されるため、正確なゼロの結果の符号はこれらの行では検査されません。

認証の失敗は不合格とする

bin_float は、認証された誤差限界と有界な精密化ループを用いて初等関数を評価します。丸めを認証できない場合は、誤っているかもしれない値ではなくエラーを返します。実行器はそのようなエラーを専用のメッセージ付きの不合格行として数えるため、コーパスの実行はすべての行で認証が成功したことの証明にもなります。

行番号を ID とする

これらの形式では行に名前がないため、ID は op:LINE（または sqrt:LINE、pow:LINE）です。固定されたファイルが変わらない限り ID は安定しており、それは testdata/bin_float/corpora.json の SHA-256 による固定が保証します。

正しさ／不変条件

合格の健全性。 MPFR の $y$ が $f(x)$ の正しく丸められた値であれば（MPFR はこれを保証します）、平方根またはべき乗の行が合格することは $\hat y = \circ_{p,\rho}(f(x))$ が正確に成り立つことを示し、初等関数の行が合格することは、ゼロの符号と NaN のペイロードを除いて同じことを、記載されたフラグとともに示します。

カウンタの恒等式。 解析されたすべての行が実行されるため、 $\text{total} = \text{passed} + \text{failed}$ であり、解析された行数は total_cases に等しくなります。

決定性。 各行の結果はその行のみに依存します。

解析の全域性。 コメント以外のすべての行は行データまたは診断になり、ドキュメントが返されるのは診断が 1 つもない場合に限られます。

既知の中断。 pow、hypot、atan2 の初等関数の行で第 2 オペランドが - であるものは、パーサーを通過し、実行時に中断（abort）します（実行器が欠けたオペランドに対して unwrap を呼び出すため）。

却下した代替案

10 進文字列の比較。 10 進出力には独自の正しく丸められた変換が必要になります。16 進数の仮数部であれば正確に比較できます。
IEEE 形式での実行。 範囲の効果と丸めの効果が混ざり、高精度の行（精度 113 以上）の大半が実行不可能になります。
テスト時に MPFR をリンクすること。 データは小さな C プログラムによって一度だけ生成されて固定されるため、MoonBit のテスト実行には C への依存が不要で、すべてのターゲットで動作します。

境界

平方根の行は値のみを検査し、フラグは検査しません。
初等関数の行は、ゼロの結果の符号や NaN のペイロードを検査しません。
指数範囲、非正規化数、オーバーフロー処理は検証されません。
上記の 3 つの形式のみを理解します。汎用の MPFR テストファイルリーダーはありません。
ファイルの読み取り、形式の検出、終了コードは cli/mpfr_expr_cli にあります。

L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, P. Zimmermann, “MPFR: A multiple-precision binary floating-point library with correct rounding”, ACM TOMS 33(2), 2007. ↩
IEEE 754-2019 の第 7.2 節（無効演算）と第 7.3 節（ゼロ除算）、および推奨される初等関数については第 9.2 節。 ↩