bin_float 適合性
この文書は 0.8.0 における 2 進浮動小数点の意味論と検証境界を記録します。有限のテストが全通過しても、すべての実数入力に対する形式的証明を意味しません。
標準・論文・参照実装
- IEEE 754-2019：interchange format、丸め方向、符号付きゼロ、NaN、例外、丸め前/後 tininess の意味論。
- Fousse、Hanrot、Lefèvre、Pélissier、Zimmermann、 MPFR: A Multiple-Precision Binary Floating-Point Library with Correct Rounding、 ACM TOMS 33(2), 2007：厳密結果を一度だけ丸める任意精度モデル。
- John Hauser による Berkeley の SoftFloat と TestFloat（リリース 3e）が、独立に生成された IEEE の結果・フラグのベクトルを提供します。
数学的意味論とアルゴリズム
有限かつ非ゼロの BinFloat は次の 2 進有理実数を表します。
(-1)^negative * coefficient * 2^exponent2（coefficient は非負の BinCoeff）
有限の係数は 2 の因子を取り除くことで正規化されますが、ゼロの符号は観測可能なまま保たれます。無限大、qNaN、sNaN、NaN のペイロード、NaN の符号は、番兵としての有限値ではなく明示的な状態です。
add_ctx、sub_ctx、mul_ctx、div_ctx、sqrt_ctx、pow_int_ctx は、IEEE 特殊値を先に解決し、dyadic/有理数または平方根の境界で厳密な数学結果を求め、目標精度・方向で一回だけ丸め、最後に指数範囲/subnormal の量子化と五つの IEEE フラグを導出します。テスト ID やテスト値に基づく分岐はありません。
- IEEE の特殊ケースは有限の算術より前に解決されます。
- 有限の加算、減算、乗算は厳密な 2 進有理数の結果を用います。除算は厳密な整数の商と剰余による判定を用います。平方根は厳密な整数平方根と、丸めの中点との厳密な比較を用います。整数冪は方向付きの包含区間を認証し（Ziv ループ）、認証に成功しない場合は厳密な冪にフォールバックします。
- 厳密な結果は要求された精度と丸め方向へ一度だけ丸められ、その後に指数範囲・非正規化数の量子化が適用されます。
- 返される
BinaryFlagsは、その数学的な結果から導かれます。inexact、underflow、overflow、division-by-zero、invalid-operation です。
binary16 の 0x0400 * 0x3BFF は 0x0400 になりますが、 inexact | underflow です。after-rounding tininess は最終 normal encoding ではなく、目標精度で丸めた無界指数の結果から判定します。
いかなる演算も、テストの識別子、テストの値、コーパスの形式によって分岐しません。コーパスのインタプリタは、公開されたコンテキスト付き演算を包むアダプタです。
固定コーパスと結果
BinaryInterchange は IEEE の binary16、binary32、binary64、binary128 のビットパターンをデコード・エンコードします。BinaryContext は精度、丸め方向、対になった指数の上下限、および丸め前・丸め後の極小性（tininess）検出を保持します。エンコードとコンテキスト付き算術はどちらもステータスフラグを返します。通常の演算子は無制限の最近接偶数丸めコンテキストを用い、意図的にそれらのフラグを公開しません。
TestFloat アダプタにおける NaN の比較は、期待される結果が NaN である場合に限りクラス単位で行われます。これは有限値の比較を緩めたものではありません。NaN でないエンコードのビットと、すべての例外ビットは厳密に一致しなければなりません。これは、新たに生成される NaN のペイロードの選択を IEEE が許容していることを反映しています。実装自体は、選ばれた入力 NaN の符号とペイロードを保持し、signaling NaN を quiet NaN にします。
宣言されたコーパスと結果
完全ゲートは testdata/bin_float/README.md に定義します。
| ソース | 範囲 | 結果 |
|---|---|---|
| TestFloat 3e level 1、seed 1 | 4 format × 5 arithmetic operation × 5 rounding × 2 tininess | 7,461,360 / 7,461,360 |
| TestFloat 3e level 1、seed 1 | 4 format × mulAdd（5 rounding × 2 tininess）、rem、roundToInt と四つの integer conversion（5 rounding × exact/非 exact）、六つの comparison predicate | 246,766,512 / 246,766,512 |
MPFR 4.2.2 tests/data/sqrt | 実行可能な 16 進 sqrt 行すべて | 1,055 / 1,055 |
MPFR 4.2.2 pow_si フィクスチャ | 4 precision × 5 supported rounding × 6 input | 120 / 120 |
| MPFR 4.2.2 初等関数フィクスチャ | 29 operation × 3 precision × 6 rounding × 4 fixed-seed input | 2,088 / 2,088 |
| optional MPFR elementary stress、seed 20260715 | three-operation 以上の各 family で 100,000 case 以上 | 966,744 / 966,744 |
| コミット済み smoke | TestFloat、sqrt、pow_si、elementary witness | 2,451 / 2,451 |
| TestFloat 3e レベル 2 | binary16 の全 declared operation/direction/tininess | 50,205,600 / 50,205,600 |
binary16 の level-2 の結果は追加のストリーミング負荷試験の証拠であり、はるかに大きい binary32/64/128 の level-2 スイートについて主張するものではありません。アーカイブ、ファイルとそのダイジェストは testdata/bin_float/corpora.json に固定されています。ランナーは TestFloat level 2 を検証済みの有界チャンク単位でストリーミング実行しますが、level 2 は任意の負荷試験スイートであり、上記の結果の主張には含まれません。966,744 行の MPFR 実行も同様に任意の生成負荷試験の証拠であり、再現可能なリリース境界は引き続きハッシュで固定された 2,088 行のフィクスチャです。
主張の境界
Evidence の安定性
固定 matrix が release evidence の境界です。新しい operation には新しい corpus contract と oracle が必要です。
four interchange format の contextual add/sub/mul/div/sqrt、fused multiply-add、remainder、roundToIntegral（通常と exact）、符号付き/符号なし 32/64 bit 整数への convertToInteger（通常と exact）、quiet/signaling の equal/less/less-or-equal predicate に加え、24、53、113 bit と六つの project rounding mode における 29 elementary operation を検証します。invalid な整数変換は flag のみ比較します（SoftFloat は platform 依存の sentinel を返し、API は None を返すため）。format 間変換、min/max、total order、nextUp/nextDown、scaleB/logB、decimal character 変換（package test で検証）の TestFloat 適合性、および全 IEEE 754 operation または全実数入力の適合性は主張しません。nearest-away は MPFR が要求する mpfr_round_nearest_away_begin/end protocol で生成し、禁止されている MPFR_RNDNA を general elementary function に直接渡しません。
日常の確認は just conformance smoke binary、固定 full gate は just gate binary を実行します。