機械翻訳であり、ネイティブスピーカーによる確認は行われていません。英語版が基準です。

検証とエビデンスGitHub で編集ソース：docs/REPRODUCIBILITY.md

再現性と来歴

Kshana は再現可能であるように作られています。同じ入力は同じ結果を生み、ビルド成果物は、それを生成したソースまでたどることができます。この文書は、何が保証され、何が保証されず、その保証がどのように担保されているかを正確に述べます。

決定論の保証#

エンジンは、実時間の時計にも、実行スレッドにも依存せず、シードのない乱数も使いません。確率的な過程はすべて、シナリオの seed をキーとする ChaCha8Rng ストリームで駆動され、固定された順序で抽出されます。その帰結は次のとおりです。

性質 保証されるか 担保の手段
同じシナリオ、同じマシン → バイト単位で同一の result.json 可 scripts/check-reproducible.sh（基準シナリオを二回実行し、SHA-256（SHA：Secure Hash Algorithm）を比較）
同じシナリオ → フィールドごとに同一の性能指標 はい、プラットフォームごと tests/golden.rs が、四つの基準シナリオのすべての性能指標（FoM）を固定
シナリオ入力ハッシュ（scenario_hash）はプラットフォームに依存しない 可 正準形のシナリオの内容アドレス指定の SHA-256 を、tests/golden.rs で固定
入力のフィンガープリントと出力の形状は OS（オペレーティングシステム）間で同一 可 tests/cross_platform_golden.rs は、シナリオごとに正確な SHA-256 を固定（十のシナリオで、tests/golden/ に .sha256 ファイルが一つずつ）し、3 OS の CI（継続的インテグレーション）マトリクスで検証
出力の値は OS（ubuntu/macOS/Windows）間で一致 はい、1e-6 まで reproducibility-matrix CI ジョブが、三つすべての OS で golden.rs（1e-6）、sgp4_verification.rs（2e-5 km）、determinism.rs を実行
低軌道（LEO）の航法メッセージのフレームは、WebAssembly（WASM）ビルドを含め、すべてのプラットフォームとすべてのビルドプロファイルで同じバイト列になる 可 src/portable_math.rs（leo-navmsg 種別のすべての超越関数とすべての正規偏差は、純 Rust の libm クレートを通る）。leo_navmsg::tests::the_encoded_frame_is_the_same_bytes_on_every_platform は、プラットフォームによる制限なしにフレーム全体を固定
シードを与えたインデックスの抽出（ブートストラップ再標本化、シャッフル）は、32 ビットと 64 ビットのターゲットで同じ 可 portable_math::uniform_index は常に u64 としてサンプリングします。portable_math::tests で固定
どこでも同じツールチェーン 可 rust-toolchain.toml がチャネルを固定し、scripts/check-toolchain.sh がずれたらビルドを失敗させ、CI とリリースは同じバージョンを固定
同じ依存関係の集合 可 Cargo.lock がコミットされ、cargo metadata --locked が SBOM（ソフトウェア部品表）に使われる

コマンドラインの実行はすべて、レポート（<scenario>.report.json と .report.html）に再現性の記録も書き出します。エンジンのバージョン、シナリオファイルと結果ドキュメントの SHA-256、シード、プラットフォーム、そして正確なコマンドで、tests/advanced_report_cli.rs がこれを再実行してバイト単位で同一の結果を得ます。レポート自体も実行の純粋関数です。scenarios/clock-holdover.toml を二回実行すると、同じ report.json がバイト単位で書き出されます。REPORTS.md を参照してください。

プラットフォームをまたぐ場合の注意（およびゴールデンテストの扱い）#

数値結果は、ある一つのプラットフォーム上ではビット単位で同一ですが、プラットフォーム間では、最終桁の数単位（ULP：unit in the last place）で異なることがあります。原因はプラットフォームの数学ライブラリです。sqrt、ln、exp などは、IEEE-754（IEEE：Institute of Electrical and Electronics Engineers）で正しく丸められることが要求されていないため、Linux（glibc、GNU C ライブラリ）、macOS、Windows はそれぞれ異なる最終ビットを返し得ます。長い実行では、この ~1e-16 の差が累積して、相対でおよそ ~1e-12 になることがあります。

最終桁の差を、元よりも大きくする要因が二つあり、どちらも仮定ではなく測定されたものです。適応型の積分器は、誤差の推定値から五乗根を通じて次のステップを選ぶため、最終桁の一単位の違いがステップ列を変え、二つのプラットフォームは積分の許容差の範囲でしか一致しなくなります。反復型の推定器（最小二乗フィット、軌道決定フィルター）は、収束までの経路が異なることがあります。そのいずれかに基づく種別は、個々のフィールドでプラットフォーム間に 1e-6 を超える差が出ることがあります。src/test_support.rs は、単体テストについて同じ領域を記録しています。

ビルドプロファイルも、同じ一台のマシン上で同様に影響します。macOS の最適化ビルドは、一つの引数の正弦と余弦を、システムの結合ルーチンへの単一の呼び出しにまとめますが、その正弦は、200,000 個の引数のうち 379 個で、単独の sin と最終ビットが異なります。最適化なしのビルドでは二回の呼び出しになります。aarch64 の macOS で 138 個のシナリオファイルを測定したところ、一つのソースのデバッグビルドとリリースビルドは、102 個で結果ドキュメントがバイト単位で同一でした。残りの 36 個は最終桁が異なります。28 個は 1e-6 以内、一つ（leo-ppp-convergence）は 2.8e-6 で、七つのキャンペーンはメンバー実行のダイジェストのみが異なります。ラベル、件数、判定が異なるものはありません。したがって、上記のバイト単位の同一性の保証は、一つのビルド、つまり同じバイナリを二回実行する場合に限られます。

シードを与えた正規乱数の抽出は、三つ目の、はるかにまれな要因です。サンプラーはまれな分岐でホストの指数関数と対数関数を呼び出し、ネイティブ版と WASM 版の間で、百万回に一回ほどの抽出が最終ビットで異なります。

出力が離散的な場合、最終桁の違いはまったく許容できないため、その種別はホストのライブラリではなく src/portable_math.rs で計算されます。leo-navmsg 種別がその最初のものです。そのバイナリフレームは送信される整数であり、同じシナリオが、リリースビルド、同じソースのデバッグビルド、ブラウザーで、かつては三つの異なるフレームにエンコードされていました。現在は、三つすべてで同じバイト列になります。

このため、ゴールデンテストは浮動小数点の出力について、プラットフォームをまたぐ単一のハッシュを固定しません。それは脆く、別の OS 上で正しくビルドされたものを正直に失敗させてしまうからです。その代わりに、次のようにします。

  • tests/golden.rs は、各性能指標を 1e-6 の相対許容差で固定します。これは、実際の退行（値を数パーセント単位で動かす）よりも四桁厳しく、それでいて、プラットフォーム間の数学ライブラリ（libm）のゆらぎよりはずっと緩い値です。格子で制限されるフィールド（ホールドオーバーの秒数）と、厳密にゼロのフィールドは、厳密に固定されます。
  • scenario_hash、すなわち入力の内容ハッシュは、プラットフォームに依存せず、厳密に固定されます。
  • tests/cross_platform_golden.rs は、プラットフォーム間で同一である射影、すなわち入力のフィンガープリントと出力の形状（フィールド名、ネスト、葉の型、配列の長さ。決定論的な格子の算術で固定され、浮動小数点の値は含まない）について、正確な SHA-256 を、tests/golden/ にシナリオごとにコミットして固定します。これにより構造上の退行は厳密に捕捉され、上記の許容差による固定は値の退行を捕捉します。
  • scripts/check-reproducible.sh は、同じマシン上での二回の実行でバイト単位で同一の出力になることを強制します（決定論の保証）。
  • reproducibility-matrix CI ジョブは、上記の四つのテスト（cross_platform_golden、golden、determinism、sgp4_verification）を ubuntu-latest、macos-latest、windows-latest で実行します。これにより、単一の OS に頼るのではなく、プッシュのたびにプラットフォーム間の再現性が確認されます。形状と入力のゴールデンは厳密に、数値は 1e-6 まで、SGP4（Simplified General Perturbations 4）の状態は 2e-5 km までです。

固定した数値を再生成する必要がある場合（たとえば意図したモデル変更の後）は、各基準シナリオを実行し、表示された FoM の値を tests/golden.rs にコピーして、その変更を CHANGELOG.md に記録してください。

ソフトウェア部品表（SBOM）#

scripts/gen-sbom.sh は、Kshana の成果物に含まれるすべてのクレートを、正確なバージョン、ソース、ライセンスとともに列挙する CycloneDX 1.5 の SBOM を出力します。これは cargo metadata --locked に基づく依存関係なしのジェネレーター（ツールチェーンだけで動作します）で、kshana パッケージから、通常の依存関係とビルド依存関係のみをたどって解決グラフを走査します。開発用の依存関係（sgp4 のようなテスト専用のクレート）は、どの成果物にも含まれないため除外されます。

このグラフは、出荷される成果物のビルドに使われる機能セットの和集合です。既定のビルド（ライブラリと CLI（コマンドラインインターフェース））、--features python（PyPI（Python Package Index）のホイール。その pyo3 のチェーンが外部関数境界）、--features wasm（この同じ SBOM を tarball 内に含む npm パッケージ）です。ホイールは複数のオペレーティングシステム向けに出荷され、npm パッケージは WebAssembly を対象とするため、すべてのターゲットのプラットフォーム条件付き依存関係が含まれます。一つの文書が三つすべての成果物を対象としているため、どれか一つにとっては上位集合になります。現在は 107 個のコンポーネントを列挙しており、その数は tests/fixtures/reproducibility_software_assurance/ で固定されています。単体の kshana-mcp サーバーは独自のマニフェストを持ち、この SBOM では記述されません。

出力は決定論的です。同じ依存関係の集合からは、バイト単位で同一の文書が得られ、シリアル番号もタイムスタンプではなく、ソート済みのパッケージリストから導出されます。

リリースのワークフローは SBOM（kshana-sbom.cdx.json）を生成して、タグ付けされたすべてのリリースに添付し、公開のワークフローは、それを PyPI のホイールの隣と npm パッケージの中にも同梱します。

ビルドの来歴#

リリースのワークフローは、GitHub リリースに添付するすべてのファイルを対象とする SLSA（Supply-chain Levels for Software Artifacts）のビルド来歴アテステーション（actions/attest-build-provenance）を作成します。対象は、各プラットフォーム向けのコマンドラインバイナリ、kshana-mcp サーバーのバイナリ、SBOM、検証サマリー、SHA256SUMS です。利用者は gh attestation verify で、成果物がこのリポジトリのリリースのワークフローによってこのソースからビルドされたことを検証できます。これにより、「ここにバイナリがある」と「そのソースまでたどれるバイナリがある」との間の隔たりが埋まります。たとえば、v0.28.0 の SBOM の場合：

curl -sLO https://github.com/AshfordeOU/kshana/releases/download/v0.28.0/kshana-sbom.cdx.json
gh attestation verify kshana-sbom.cdx.json --repo AshfordeOU/kshana