性能とセマンティクスの監査

このガイドは、リポジトリの性能ベースラインであるリリース 0.7.1 を構成する最適化の監査を記録したものです。最適化された経路、レビュー中に見つかったセマンティクス上の修正、各高速経路が一般経路とまったく同じものを返すことの証明、そして性能に関する主張の根拠の範囲を列挙します。現在のブランチを含むその後の作業では新たな性能測定は追加されていないため、この監査は引き続き最適化経路の基準となります。

範囲

この監査は、リリース 0.7.0 に続くコミット 69084bc、7904016、23005ed、4fd41ad に加えて、0.7.1 のリリースレビュー中に行われた GDA 係数ヘルパーと区間の回帰修正を対象とします。観測された挙動、規範的な期待、実装上の選択、受け入れの証拠を、それぞれ別個の事実として扱います。

問題マトリクス

行	分類	観測	期待値	変更	受け入れの証拠
GDA 係数カーネル	実装上のギャップ	GDA の高速経路が、小さな表現、剰余のみの除算、半べき比較を追加した	係数の恒等式、コホート、フラグ、トラップ、スティッキーなステータスは不変	正準な `GdaCoeff` 演算を使い、共有の GDA ファイナライザを維持する	package 93 tests、frontend 8 tests、`official` 64,986/64,986、`official0` 16,124/16,124
IEEE 十進の経路	セマンティクス上のリスクを伴う最適化	厳密除算と上限付き除算の経路が、繰り返される汎用処理を省略する	厳密な十進の結果、丸め、量子、フラグ、例外値が IEEE の挙動と一致する	高速経路を有限領域、因数、上限、ファイナライズの述語で保護し、それ以外はフォールバックする	package 94 tests、four-target IEEE 15,763/15,763
二進 IEEE の経路	セマンティクス上のリスクを伴う最適化	exact-top による順序付け、分割された丸め／スティッキーの抽出、係数によるディスパッチが、より広い範囲の処理を置き換える	コンテキスト付きの値、丸め、フラグ、符号付きゼロ、交換形式のビットが同一	厳密な係数の構築を維持し、すべての結果をコンテキスト付き丸めに通す	package 68 tests、binary 7,464,503/7,464,503
区間端点のディスパッチ	セマンティクス上の逸脱、修正済み	最適化された `pown` が符号領域をまたいで端点の方向を再利用していたため、負の区間で $\underline{y} > \overline{y}$ になるか、1 ulp を失うことがあった	返されるすべての区間が順序付けられ、厳密な像を含む	単調性から端点を選び、各候補を外向きに丸める。負の半軸のテストを追加する	パッケージテスト 42 件、整数べき 174/174、strict ITF1788 4,656/4,656
リリースドキュメント	ドキュメントのギャップ	0.7.0 がまだ現在のベースラインとして記載されていた	現在の参照は新しいベースラインを記載し、履歴は変更履歴に残す	メタデータを更新し、この監査を追加する	`python3 tools/doc_quality.py`

最適化の証明

厳密な係数の経路

係数 $a \ge 0$ と除数 $d > 0$ に対し、剰余は次のとおりです

r = a - \left\lfloor \frac{a}{d} \right\rfloor d, \qquad 0 \le r < d .

剰余のみのカーネルは商と剰余を求めるカーネルと同じ $r$ を返すので、観測可能なすべての剰余とユークリッドの互除法のすべてのステップを保ちます。GDA の半べき述語は、 $a$ と $5 \cdot 10^{\,\operatorname{digits}(a) - 1}$ を、先頭の十進桁と残りの部分が非零かどうかによって比較します。これは厳密であり、浮動小数点による推定ではありません。

IEEE 十進の厳密除算経路は、まず $g = \gcd(c_x, c_y)$ で約分します。商 $c_x / c_y$ が有限の十進展開を持つのは、約分後の分母 $c_y / g$ が 2 と 5 以外の素因数を持たないときであり、かつそのときに限ります：

\frac{c_x}{c_y} = \frac{c_x / g}{2^{i} 5^{j}} = \frac{(c_x / g) \cdot 2^{k-i} 5^{k-j}}{10^{k}}, \qquad k = \max(i, j).

この経路が選ばれるのはその場合だけです。厳密な係数と指数を構築し、既存のファイナライザを呼び出します。因数、上限、特殊値に関する前提条件のいずれかが満たされなければ、汎用アルゴリズムに戻ります。この最適化が変えるのは厳密値に至る経路であって、IEEE の丸めやフラグの規則ではありません。

二進のコンテキスト付き経路

有限の二進有理数値 $c \cdot 2^{e}$ に対し、binary_exact_top(c, e) は最上位のセットビットの指数 $e + \operatorname{bitlen}(c) - 1$ です。これらの top を比較することは、末尾の 2 のべきが異なる係数も含め、桁合わせ前に絶対値を比較することと等価です。遠く離れた加数が捨てられるとき、分割処理は最初に捨てられるビット（丸めビット）と、それ以降のすべてのビットの OR（スティッキービット）を保持します。これらはまさに丸め判定の入力です。切り捨てた絶対値 $t$ と、1 ulp に対する捨てられた端数 $f \in [0, 1)$ について、

\text{round bit} = [f \ge \tfrac{1}{2}], \qquad \text{sticky bit} = [f \notin \{0, \tfrac{1}{2}\}],

そしてすべての IEEE の丸め方向は、 $t$ の最下位ビット、符号、およびこの 2 つのビットの関数です。したがって高速経路は、巨大な桁合わせ済みの係数を実体化することなく、同じ丸め入力を与えます。

方向付き区間の経路

区間演算は包含の不変条件 $f(X) \subseteq [\underline{y}, \overline{y}]$ と格納の不変条件 $\underline{y} \le \overline{y}$ を保たなければなりません。厳密な端点候補 $y$ に対し、 $\operatorname{RD}(y)$ は有効な下側の証明書であり、 $\operatorname{RU}(y)$ は有効な上側の証明書です。pown の分岐は $x \mapsto x^{n}$ に対する次の単調性の表を用います：

ドメイン	$n > 0$ 奇数	$n > 0$ 偶数	$n < 0$ 奇数	$n < 0$ 偶数
負の半軸	増加	減少	減少	増加
正の半軸	増加	増加	減少	減少
ゼロを含む区間	端点の順序	$0$ から外向きに丸めた最大値まで	極：分割または Entire	極：分割または Entire

実装はまず数学的な端点を選び、その役割が要求する方向を適用します。偶数の $n > 0$ でゼロをまたぐ区間では、有限な 2 つの極値候補はどちらも上限のために上向きに丸められます。その後 quantize_interval がもう一度外向きに丸めます。この証明は宣言された演算と精度の契約に限定されたものであり、サポートされていない逆演算については何も主張しません。

性能の証拠

領域	測定	解釈
二進、十進、GDA、区間のカーネル	`just bench all --target native`	4 つの Maremark スイートすべてが有効な成果物を生成した
二進の二乗ポリシー	`just bench auto-tune --target native`	ターゲット固有のポリシー成果物。生の観測値は単調でない場合があり、普遍的なしきい値ではない
IEEE と GDA の高速経路	ベンチマークパッケージのテストと適合性ゲート	高速な経路が許容されるのは、セマンティクスのオラクルがグリーンである間だけ
区間端点のディスパッチ	`src/bench/ball_float` と strict ITF1788	ordered な outward enclosure が成立する場合だけ cost reduction を受け入れる

生成された成果物は .tmp/bench/ 以下に置かれ、API データとして公開されることはありません。クロスオーバーを採用する前に、ターゲットのハードウェアでコマンドを再実行してください。このワークロードは監査対象のツリーに関する証拠であり、すべてのリリースでの高速化、ターゲット間の同等性、レイテンシの上限を証明するものではありません。

受け入れマトリクス

チェック	結果
`sh tools/run_moon_clean_exec.sh test src/decimal_gda --target native --deny-warn --frozen --no-parallelize`	93/93 合格
`sh tools/run_moon_clean_exec.sh test src/decimal --target native --deny-warn --frozen --no-parallelize`	94/94 合格
`sh tools/run_moon_clean_exec.sh test src/bin_float --target native --deny-warn --frozen --no-parallelize`	68/68 合格
`sh tools/run_moon_clean_exec.sh test src/ball_float --target native --deny-warn --frozen --no-parallelize`	42/42 合格
`just gate binary 8`	7,464,503/7,464,503 合格
`just gate decimal 8`	15,763/15,763 合格
`just gate decimal_gda 8`	64,986/64,986 と 16,124/16,124 passed
`just gate interval 8`	4,656/4,656 合格
`python3 tools/doc_quality.py`	合格

これらの件数は監査対象のツリーについてのものです。ゲートはその後拡大しています（二進のゲートは現在 IEEE 演算の完全なマトリクスを実行します）。現在の主張は検証に列挙されています。

レビュアーによる自己レビュー

貢献：合格。この監査は、説明のない高速化ではなく、具体的な最適化の境界と修正されたセマンティクス上の不具合を記録しています。
明瞭さ：合格。各証明は表現、単調性、丸め方向、証拠を分けて扱っています。
実験の強さ：再現が必要。ネイティブの成果物は有効ですが、ノイズの多い自動チューニングの観測値は、しきい値を採用する前に再測定すべきです。
完全性：宣言された固定コーパスについては合格。すべての標準演算やすべての実入力を網羅するものではありません。
健全性：負の半軸の回帰修正と IEEE 1788 の完全なゲートを経た後、対象となる分岐について合格。

主張と証拠の対応表

宣言	evidence	ステータス
高速な係数経路は宣言された数値結果を保つ	厳密カーネルの恒等式、パッケージテスト、IEEE と GDA の適合性	declared API と precondition の範囲で supported
区間の `pown` は順序付けられた外向きの包含区間を保つ	monotonicity table、negative-half-axis regression、4,656 strict ITF1788	宣言された順方向の区間演算について裏付けあり
最適化経路は性能監査済みである	native Maremark `all` と `auto-tune` artifact	測定の証拠としては裏付けあり。普遍的な速度の主張ではない
すべてのターゲットと演算で同等の性能を持つ	ターゲット間で対になる成果物がない	主張しない

制限事項

セマンティクス上の主張は、固定されたコーパス、公開された演算、ターゲット固有の精度規則、および明示的なフォールバックの契約によって範囲が限定されます。0.6.1 の初等関数マニフェストは引き続き初等関数の性能ゲートの比較ベースラインであり、0.7.1 がその候補です。ベンチマークを改善するためだけに、公開 API、丸め規則、エラーシグナル、包含区間の契約を変更することはありません。