consistency の設計

設計目標

luna-poly は、2 つの層とその表現が同じ数学を表すことを約束しています。consistency はその約束を moon test で実行されるテストに変えます。このテストは両方のファサードに依存するパッケージに置かれるため、どちらの層のテストももう一方の層について知る必要がありません。

数学的背景

各表現 $\rho$(dense、term、sparse、context。イミュータブルまたはミュータブル)には、多項式環への解釈 $[\![\cdot]\!]_\rho$ が伴います。一貫性とは、すべての演算が解釈と可換であるという主張です:

$$[\![\, a \mathbin{\mathrm{op}_\rho} b \,]\!]_\rho = [\![ a ]\!]_\rho \mathbin{\mathrm{op}} [\![ b ]\!]_\rho ,$$

さらに、表現間の変換が解釈を保つことも含みます。テストは具体的な入力に対してこれらの等式の具体例を検査します。

設計上の判断

独立したホワイトボックスパッケージ

この検査には immut と mutable の両方が必要ですが、mutable はすでに immut に依存しています。どちらかの層に置くと、依存関係が逆転するか絡み合ってしまいます。ホワイトボックステスト (core_wbtest.mbt) を持つ専用パッケージが、テスト時にのみ Luna-Flow/arithmetic、immut、mutable をインポートし、公開 API には何も寄与しません。

検査する内容

• 密多項式に関する層の一致: 係数、積、合成、評価が immut と mutable で等しいこと。
• 自然数乗: PowNatChecked::pow_nat_checked(p, 0, ctx) が両方の層で 1 であり、pow(5) が一致すること。
• 分離: to_immut の後でミュータブルな多項式を変更しても、スナップショットは変わらないこと。
• 多変数の一致: 項と疎の格納、イミュータブルとミュータブルが、同一の評価結果と同じ累乗を生むこと。
• 能力インターフェース: UnivariatePolynomial、MultivariatePolynomial、Zero、One を境界とする関数と ops() レコードが、両方のファサードを通じて動作すること。形状が期待どおりのアリティ、項数、両立性を報告すること。
• チェック付きの契約: *_checked メソッドが、負のインデックスや短すぎる評価点に対して中断 (abort) せずに None を返すこと。
• ミュータブルなコンテキストの委譲: 部分評価とその失敗ケースがイミュータブルな振る舞いと一致すること。

単一の表現に関する代数法則(正規化の冪等性、加法単位元、Karatsuba 法と筆算法の乗算の比較、係数の最小境界)は、検査対象のコードの隣にある immut/laws_wbtest.mbt に置かれています。

正しさ / 不変条件

このパッケージには実行時のコードがありません。その不変条件は moon test が成功すること、すなわち上のすべての等式がテストされた入力で成り立つことです。

採用しなかった代替案

• mutable 内のテスト にすると、ミュータブル層のテストが暗黙のうちにイミュータブル層の内部に依存してしまい、他の層で再利用することもできません。
• 表現のすべての組についての網羅的なプロパティテスト はテスト時間を何倍にも増やします。このパッケージは代表的な演算を検査し、プロパティテストは個々の法則の側に置いています。

境界

• テストは有限個のサンプルであり、証明ではありません。
• 公開 API はありません。ここにあるものはインポートされることを想定していません。