consistency の設計

設計目標

floating には主張が重なり合う 4 つの数値コアがあります。2 進値を 10 進に変換して戻したものは同じ有理数を表さなければならず、checked ラッパーはコアと同じ値を与えなければならず、区間はスカラー演算の厳密な結果を包含しなければならず、すべてのコアは同じ internal の規則で丸めなければなりません。各パッケージ自身のテストからは他のパッケージは見えません。consistency は、こうしたパッケージ横断の法則を書き下して実行する唯一の場所です。

数学的背景

各コアのすべての有限値は有理数を表します。$\llbracket\cdot\rrbracket$ を値を $\mathbb{Q}$ に写す写像とします（semantic で実装され、internal.ExactRat を正準形とします）。スイートが検査する法則には 3 つの形があります：

• 一致： パッケージ $A$ の値 $x$ とパッケージ $B$ の値 $y$ が同じ入力を表すとき、両方の演算が厳密であれば $\llbracket f_A(x) \rrbracket = \llbracket f_B(y) \rrbracket$ であり、そうでなければ結果は同じ実数を 2 つのパッケージがそれぞれ丸めたものである。
• 厳密なオラクル： ヘルパーまたは演算が BigInt や有理数による計算と等しい。例えば round_positive_div を $\lfloor n/d \rfloor$ と丸め表に対して、digits10 を 10 の累乗に対して検査する。
• 包含： 区間演算 $F$ と点演算 $f$ について $x \in X \Rightarrow f(x) \in F(X)$ が成り立ち、包含関係は全順序ではなく半順序として振る舞う。

表現に関する法則も検査されます。GDA の結果は正しいコホート、符号付きゼロ、NaN のペイロードを保ち、交換形式の符号化はビット単位で往復変換できます。

設計上の判断

ホワイトボックステストのみ

このパッケージにはテスト以外のソースファイルがなく、コアを for "wbtest" でのみインポートします。そのためライブラリのビルドに含まれることはなく、保守すべき API もありませんが、内部ヘルパーは利用できます。

公式コーパスに由来する固定の証拠ケース

多くの 10 進テストは、公式 decTest スイートの行を名前付きの証拠ケースとして使います。これらは、かつてパッケージ間で食い違った正確なケースを、プロセス内で、コーパスをダウンロードせずに固定します。

期待値よりオラクル

可能な場合、テストは出力文字列をハードコードするのではなく、期待される結果を（BigInt、ExactRat、semantic で）独立に計算します。これにより書式が変わっても法則は意味を保ちます。

正しさ／不変条件

• 成功した実行は、述べられた各法則がその証拠ケース上で成り立つことを示します。これは有限の根拠であり、すべての入力に対する証明ではありません。
• テストは決定的でターゲットに依存しないため、native、Wasm、JavaScript で同じ実行を行えば同じ主張が検査されます。

却下した代替案

• パッケージ横断テストを各パッケージに置く。 コア間にテスト専用の依存サイクルが生じます。
• プロパティベースのランダムテストのみ。 ランダムな入力はコホートの境界や同点にほとんど当たりません。固定の証拠ケースなら当たります。

境界

• 公開 API も実行時コードもありません。
• 外部コーパス（それは適合性フロントエンドの役割です）も性能計測（bench パッケージ）も扱いません。