アーキテクチャ

floating は、明示的な数値ドメインと、それを取り巻く薄い合成・パース・検証レイヤーで構成されています。中心となる原則は、数値意味論を純粋かつ明示的に保ち、ファイル、プロセス、コーパス、ベンチマークをリポジトリの周縁に置くことです。本ガイドでは、パッケージをこれらのレイヤーに対応付け、一つの演算が数値コアを通過する流れを追い、各レイヤーが守る不変条件を示します。

レイヤーマップ

レイヤー	Package	責務
共通語彙	`def`	`Sign`、`PartialOrder`、`Floating` トレイト、述語、再エクスポートされた `arithmetic` の型
scalar domain	`bin_float`, `decimal`, `decimal_gda`	二進、IEEE 十進、GDA 十進の値と、そのコンテキストおよびステータス
interval domain	`ball_float`	外向き丸めによる実数の包含区間（bare および decorated）
checked composition	`bin_float_checked`, `decimal_checked`, `decimal_gda_checked`, `ball_float_checked`	各ドメインのエラー、フラグ、トラップの状態を保持するパイプライン
semantic projection	`semantic`	表現に依存しない厳密な観測
syntax	`numeric_expr`	source span、literal、primitive call、callback evaluation
format frontend	`frontend/gda_expr`, `frontend/itl_expr`, `frontend/mpfr_expr`, `frontend/testfloat_expr`	一つの外部コーパス文法をパースし、型付きのケースを実行する
runtime adapter	`internal`、`internal/conformance`、`internal/runner_cli`、`cli` および `cli/*`	共有ヘルパー、サマリー、シャーディング、ファイル、JSON およびテキスト出力、終了ステータス
evidence	`consistency`、`doc_examples`、`bench` および `bench/*`、`tools/`、`testdata/`	パッケージ横断の法則、ドキュメントの例、ベンチマーク、適合性検証のオーケストレーション

パッケージ境界は moon.pkg によって決まります。パッケージ内のファイルは実装を整理するものであり、名前空間を作りません。依存関係は下向きです。すべての数値パッケージは def と internal に依存し、ball_float は bin_float の上に構築され、decimal と decimal_gda は認証付き初等関数のために bin_float と ball_float を利用し、checked パッケージはそれぞれのドメインをラップします。数値的なものがフロントエンド、CLI、ベンチマークに依存することはありません。

標準ごとの境界

普遍的な「浮動小数点値」というものは存在しません。各標準はそれぞれ独自の観測可能な状態を保持します。

ドメイン	規範モデル	演算結果
`bin_float`	任意精度の IEEE 754-2019 二進算術、binary16/32/64/128 交換形式	値 + `BinaryFlags`
`decimal`	IEEE 754-2019 十進算術、decimal32/64/128 の DPD および BID 交換形式	値 + `DecimalFlags`
`decimal_gda`	General Decimal Arithmetic Specification 1.70、スカラー演算	raised、sticky next context、optional trap を持つ `GdaOutcome`
`ball_float`	IEEE 1788-2015 の bare 区間および decorated 区間（宣言された演算集合について）	包含区間、装飾（decoration）または NaI、オプションの `BallFlags`

この分離により、GDA のトラップを IEEE のフラグとして扱う、IEEE の無限大を汎用エラーとして扱う、あるいは Empty、Entire、NaI を互換な区間の失敗として扱うといった、情報を失う変換を防ぎます。これらの各状態は数値意味論で定義されています。

数値コアのパイプライン

表現や標準は異なっていても、すべてのスカラーコアは一つの分解を共有します。

immutable operand value(s) + explicit context
  -> special-value and domain classification
  -> exact coefficient computation, or a certified enclosure
  -> one domain-owned finalization (rounding, exponent range, status)
  -> public value + explicit status

BinFloat は、クラス、符号、末尾に 0 ビットを持たない非負の二進係数、指数、精度、および NaN の状態（signaling ビットとペイロード）を保持します。Decimal と GDA の Decimal は、それぞれ符号、パッケージが所有する基数 $10^9$ の係数、量子（quantum）を表す指数、精度、および特殊状態を保持します。BallFloat は二つの BinFloat 端点、精度、Empty マーカーを保持し、BallFloatDecorated は bare 表現を変えずに装飾を追加します。

最終化（finalization）は意味論上のファイアウォールです。カーネルは厳密な和、積、商、根、あるいはガードビットやスティッキービットを計算できますが、丸められた値、コホート、フラグ、トラップ、装飾、区間端点の方向を決めるのはファイナライザだけです。ファイナライザはまた、先頭ビットについて二進実装の指数範囲 $[1 - 2^{30},\ 2^{30} - 1]$ を強制します。この範囲外の結果は、飽和した指数で格納されるのではなく、丸め方向に応じてオーバーフローまたはアンダーフローとして分類されます。

厳密値が巨大になる演算では、その値を実体化しません。遠く離れた加数はスティッキービットに縮約され、IEEE の剰余は $2^k$ 上の二乗乗算法によって巨大な被除数を $2y$ を法として縮約し、整数への丸めはシフトによって係数を分割し、区間端点の和では、もう一方より $\max(65536, p)$ ビットを超えて下位にある加数を方向付きのスティッキー項に落とします。いずれの近道も、完全な計算が与えるのとまったく同じ丸め情報とスティッキー情報をファイナライザに渡します。

アルゴリズムの選択

多倍長整数カーネルは、単一のアルゴリズムではなく段階的なセレクタを使用します。

size + shape + target + proof preconditions
  -> inline / schoolbook / Comba
  -> Karatsuba
  -> Toom-3
  -> NTT + exact CRT reconstruction
  -> exact fallback if an advanced precondition fails

除算も同様に、ターゲットでの計測が正当化する場合には、ワード除算と Knuth のアルゴリズム D から Burnikel–Ziegler 法と逆数の Newton 反復へと移行します。疎なオペランドや不均衡なオペランドには専用の経路があります。長い方の長さだけで選んだアルゴリズムでは、漸近的に節約できる以上の時間をパディングに浪費しかねないためです。

切り替え点は非公開のターゲット固有ポリシーです。これらは Maremark ベンチマーク階層（bench/*）を用いて、密、疎、正方、均衡、不均衡なデータで計測され、境界テストではすべてのカットオフの直下・直上・その点で厳密な結果を比較します。そのため Native、LLVM、Wasm、Wasm-GC、JavaScript は異なるアルゴリズムを選ぶことがありますが、同じ公開結果を返さなければなりません。

認証付き初等関数

初等関数（指数関数、対数関数、べき乗、累乗根、三角関数、双曲線関数およびそれらの逆関数）は、Ziv の戦略に倣った一つの証明契約に、二進・十進・区間の各スタックで共通して従います。¹1 A. Ziv, “Fast evaluation of elementary mathematical functions with correctly rounded last bit”, ACM TOMS 17(3), 1991. Muller ほか, Handbook of Floating-Point Arithmetic, 第 2 版, 2018, 第 10 章では、このループが解決するテーブルメーカーのジレンマが論じられています。

いかなる精緻化よりも前に、結果の $\log_2$ に対する認証済みの上下界から、コンテキストの範囲外であることが確実な結果（オーバーフロー、アンダーフロー）を判定します。
作業精度 $w = p + 64$ で、厳密値の方向付きの下側・上側の包含区間 $[\ell, h]$ を計算します。
両端点をターゲットに丸めます。丸めは単調なので、同じフラグで $\operatorname{rnd}(\ell) = \operatorname{rnd}(h)$ が成り立てば、厳密値を含む $[\ell, h]$ 内のすべての値がその結果に丸められます。
そうでなければ $w$ を $\max(32, \lfloor w/2 \rfloor)$ だけ増やして繰り返します（最大 12 回）。
どの試行でも一致しなかった場合、try_* 関数は段階、理由、精度、作業精度、試行回数を持つ CertificationFailure を返します。try でない関数は定義済みの無効な結果（二進では invalid operation を伴う quiet NaN）を返し、中断することはありません。

bin_float はスカラーの二進有理数（dyadic）証明書を所有します。ball_float はそれを端点、臨界点、極、定義域の境界へと持ち上げます。decimal と decimal_gda は、厳密な十進入力を方向付きの二進有理数の上下界に変換し、二進の証明書を実行し、認証された端点を厳密な整数演算によって十進に戻します。十進の範囲から大きく外れた端点は、同一に丸められる代表値に置き換えられるため、巨大な十進数が展開されることはありません。全域的な区間関数は $[-1, 1]$ や Entire のような安全な集合に広がることがありますが、その checked 形式は失敗を公開します。ホストの Double 近似で代用する経路はありません。

十進テキスト変換

BinFloat::from_string_ctx と to_decimal_string_ctx は、 $k$ が巨大な場合でも $10^{k}$ を展開することなく、あらゆる精度と指数について正しく丸められた結果を返します。パースでは、まず対数による見積もりから確実なオーバーフローまたはアンダーフローを判定します。指数が小さい場合は厳密な有理数 $D \cdot 10^{k}$ を丸め、大きい場合は方向付きの 10 のべきで $D \cdot 10^{k}$ を包含し、両端が同じように丸められるまで作業精度を広げます。そこではタイが起こり得ないため、この処理は必ず停止します。フォーマットでは、二進の見積もりを方向付きの 10 のべきで補正して先頭の十進指数を求め、to_shortest_string_ctx は桁数について二分探索を行います。読み戻しが桁数について単調であるため、これは妥当です。

コンテキストとステータスの流れ

暗黙の丸めモードに依存する数値パッケージはありません。

二進および IEEE 十進のコンテキストは不変の入力であり、フラグは呼び出し側が combine する明示的な出力です。
decimal_gda は、発生したフラグをステータスに含む新しいコンテキストを返し、固定の優先順位によって最大一つのトラップを選択します。
BallContext は端点の精度と指数の上下限を固定し、BallFlags を返します。
BinFloat、Decimal、GDA の Decimal は Luna-Flow/arithmetic のコンテキスト付きトレイト（AddContextual、…、ExpContextual）を実装しているため、汎用コードは三つすべてを一つの ArithmeticContext のもとで実行できます。BinaryContext::from_arithmetic_context と十進の対応する関数は、その精度、丸め、指数の上下限、クランプを引き継ぎます。
BinFloatResult と BallFloatResult は最初の ArithmeticError を保持します。
DecimalChecked は定義済みの IEEE 結果を保持し、フラグを蓄積し、認証エラーを別に保持します。
GdaDecimalChecked は一つの結果（outcome）を受け渡し、Trapped で停止し、明示的な resume_defined 遷移によってのみ再開します。

これらのラッパーは既存の意味論を合成するものであり、独自の算術を追加することも、互換性のないステータスチャネルを統合することもありません。

公開インターフェースとトレイトメソッド

何が公開されているかは、各パッケージで生成される pkg.generated.mbti が権威を持ちます。MoonBit 0.10 では、トレイト実装のメソッドは型に自動的に昇格されなくなりました。BinFloat::to_string、Decimal::add_contextual、BinFloat::sqrt_checked のようなメソッドがドット構文で呼び出せるのは、パッケージがそれを pub extend で宣言しているからであり、そのとき .mbti には pub fn Type::name として記載されます。そのように記載されていないトレイトメソッドも、トレイト経由では引き続き呼び出せます（例: Floating に対する @def.is_finite(x)）が、x.method() としては呼び出せません。

パースと実行

numeric_expr は構文データと後順コールバック評価を保持します。IO は行わず、数値バックエンドも選択しません。

各 frontend/* パッケージは一つの外部文法を所有します。

gda_expr は .decTest のディレクティブとケースをパースし、GDA の結果を実行します。
testfloat_expr は Berkeley TestFloat のベクタをパースし、形式、演算、丸め、極小性（tininess）、厳密性を結び付けます。
mpfr_expr は固定された MPFR の平方根、整数べき、初等関数の証拠データ（witness）をパースします。
itl_expr は ITF1788 の区間の行をパースし、宣言されたサポート集合を分類します。

フロントエンドは型付きのサマリーを返します。cli パッケージは、internal/conformance（シャード、ケースの処理区分、サマリー）と internal/runner_cli（オプション、ファイル、JSON）の上で、ファイル、フィルタ、シャード、レンダリング、終了コードを担当します。tools/ 以下の Python ツールは、チェックサムで固定されたデータを取得し、タスクを計画し、隔離されたターゲットとプロセスを実行し、結果を集約します。これらが MoonBit の実装を置き換えることはありません。

安定性の境界

アプリケーション向けの公開面は、def、四つの数値パッケージ、四つの checked ラッパーです。semantic と numeric_expr は暫定的な統合用の公開面です。フロントエンドはリポジトリのランナーが合成できるように公開されていますが、その互換性の保証は宣言されたコーパスに限られます。

internal と internal/*、cli と cli/*、bench と bench/*、consistency、doc_examples は実装および検証のための基盤です。シンボルが pkg.generated.mbti に現れていても、長期的なアプリケーション契約になるとは限りません。依存する前にそのパッケージの設計ページを読んでください。

Invariant

値の符号は、その非負の係数とは独立です。
有限の二進数の正規化は 2 の因数だけを取り除きます。
十進のパースは、正規化または縮約を行う演算が明示的に呼ばれるまで量子を保持します。
コンテキストの最終化だけが、有界な結果を丸め、ステータスを決定する場所です。
区間の下端は $-\infty$ 方向に、上端は $+\infty$ 方向に丸められます。
Empty、Entire、NaI、NaN、符号付きゼロ、無限大は明示的な状態として保持されます。
有限の結果が実装範囲外の指数を持つことはありません。
高速経路やフォールバックが公開される値やステータスを変えることはありません。
適合性のサマリーは選択されたケースを分割し、シャーディングは決定的です。
IO、ダウンロード、プロセスの状態、並列スケジューリングはツール側にとどめます。

拡張の規則

振る舞いは、その意味論を所有するパッケージに追加してください。包括的なトレイトを作る前に、Luna-Flow/arithmetic と Luna-Flow/luna-generic の能力トレイトを再利用してください。カーネルは非公開に、コンテキストとステータスは明示的に保ち、外部形式のパースは、その形式が安定した交換契約でない限り数値型の外に置いてください。新しいトレイトメソッドが型の公開面に属する場合は、pub extend でドット構文に昇格させてください。

適合性検証の対象範囲を拡張するには、パーサ、実行器、サポート分類、CLI スキーマ、コーパスのマニフェスト、テスト、生成されたインターフェース、ドキュメントを連携して変更する必要があります。新しい演算をパースできるだけではサポートとはみなされず、厳密な実行において定義された比較と再現可能な証拠が必要です。検証を参照してください。

A. Ziv, “Fast evaluation of elementary mathematical functions with correctly rounded last bit”, ACM TOMS 17(3), 1991. Muller ほか, Handbook of Floating-Point Arithmetic, 第 2 版, 2018, 第 10 章では、このループが解決するテーブルメーカーのジレンマが論じられています。 ↩