Traduction automatique, non relue par un locuteur natif. L'anglais fait foi.

Validation et preuvesModifier sur GitHubSource : docs/REPRODUCIBILITY.md

Reproductibilité et provenance

Kshana est conçu pour être reproductible : les mêmes entrées produisent les mêmes résultats, et les artefacts de construction peuvent être retracés jusqu'à la source qui les a produits. Ce document énonce exactement ce qui est garanti, ce qui ne l'est pas, et comment les garanties sont appliquées.

Garanties de déterminisme#

Le moteur n'a aucune horloge murale, aucune dépendance au fil d'exécution et aucun aléa non initialisé. Chaque processus stochastique est piloté par un flux ChaCha8Rng indexé par la seed du scénario, tiré dans un ordre fixe. Conséquences :

Propriété Garanti Appliqué par
Même scénario, même machine → result.json identique octet pour octet Oui scripts/check-reproducible.sh (exécute deux fois le scénario de référence, compare le SHA-256 (SHA : Secure Hash Algorithm))
Même scénario → chiffres de mérite identiques champ par champ Oui, par plateforme tests/golden.rs fige chaque chiffre de mérite (FoM) des quatre scénarios de référence
L'empreinte d'entrée du scénario (scenario_hash) est indépendante de la plateforme Oui SHA-256 adressé par le contenu du scénario canonique, figé dans tests/golden.rs
Empreinte d'entrée + forme de sortie identiques d'un système d'exploitation (OS) à l'autre Oui tests/cross_platform_golden.rs fige un SHA-256 exact par scénario (dix scénarios, un fichier .sha256 chacun dans tests/golden/), vérifié sur la matrice d'intégration continue (CI) à 3 OS
Les valeurs de sortie concordent d'un OS à l'autre (ubuntu/macOS/Windows) Oui, à 1e-6 près le job CI reproducibility-matrix exécute golden.rs (1e-6), sgp4_verification.rs (2e-5 km) et determinism.rs sur les trois OS
Une trame de message de navigation en orbite terrestre basse (LEO) a les mêmes octets sur chaque plateforme et dans chaque profil de construction, y compris la construction WebAssembly (WASM) Oui src/portable_math.rs (chaque fonction transcendante et chaque variable normale du type de scénario leo-navmsg passe par le crate Rust pur libm) ; leo_navmsg::tests::the_encoded_frame_is_the_same_bytes_on_every_platform fige une trame entière sans condition de plateforme
Les tirages d'indices initialisés par graine (rééchantillonnage bootstrap, mélanges) sont les mêmes sur les cibles 32 bits et 64 bits Oui portable_math::uniform_index échantillonne toujours en u64 ; figé dans portable_math::tests
Même chaîne d'outils partout Oui rust-toolchain.toml fige le canal ; scripts/check-toolchain.sh fait échouer la construction en cas de dérive ; la CI et la publication figent la même version
Même ensemble de dépendances Oui Cargo.lock est versionné et cargo metadata --locked sert à la SBOM (nomenclature logicielle)

Chaque exécution en ligne de commande écrit aussi une fiche de reproductibilité dans son rapport (<scenario>.report.json et .report.html) : la version du moteur, le SHA-256 du fichier de scénario et du document de résultat, la graine, la plateforme et la commande exacte, que tests/advanced_report_cli.rs ré-exécute jusqu'à un résultat identique octet pour octet. Le rapport est lui-même une fonction pure de l'exécution : deux exécutions de scenarios/clock-holdover.toml écrivent le même report.json octet pour octet. Voir REPORTS.md.

La réserve inter-plateformes (et comment les valeurs de référence figées la traitent)#

Les résultats numériques sont identiques bit à bit sur une plateforme donnée mais peuvent différer dans les derniers quelques unités de dernière position (ULP) entre plateformes. La cause est la bibliothèque mathématique de la plateforme : sqrt, ln, exp et consorts ne sont pas tenues par IEEE-754 (IEEE : Institute of Electrical and Electronics Engineers) d'être correctement arrondies, de sorte que Linux (glibc, la bibliothèque C de GNU), macOS et Windows peuvent chacun renvoyer un dernier bit différent. Sur une longue exécution, ces écarts d'environ 1e-16 s'accumulent jusqu'à peut-être environ 1e-12 en relatif.

Deux choses rendent cet écart de dernière position plus grand qu'au départ, et les deux sont mesurées plutôt que supposées. Un intégrateur adaptatif choisit son pas suivant à partir de l'estimation de l'erreur par une racine cinquième, de sorte qu'une unité de dernière position change la suite des pas et que les deux plateformes ne concordent plus alors qu'à la tolérance d'intégration. Un estimateur itératif (un ajustement par moindres carrés, un filtre de détermination d'orbite) peut suivre un chemin différent jusqu'à la convergence. Les types de scénario construits sur l'un ou l'autre peuvent différer entre plateformes de plus de 1e-6 dans certains champs ; src/test_support.rs consigne le même régime pour les tests unitaires.

Le profil de construction compte de la même façon, sur une seule machine. Une construction optimisée sur macOS fusionne un sinus et un cosinus d'un même argument en un seul appel à la routine combinée du système, dont le sinus diffère du sin isolé au dernier bit pour 379 arguments sur 200 000 ; une construction non optimisée fait les deux appels. Mesuré sur aarch64 macOS sur les 138 fichiers de scénario, une construction debug et une construction release d'une même source donnent des documents de résultat identiques octet pour octet pour 102 d'entre eux. Les 36 autres diffèrent dans les dernières positions : 28 à 1e-6 près, un (leo-ppp-convergence) de 2.8e-6, et sept campagnes seulement dans les empreintes de leurs exécutions membres ; aucun ne diffère par une étiquette, un décompte ou un verdict. La garantie d'identité octet pour octet ci-dessus vaut donc pour une construction : le même binaire deux fois.

Les tirages normaux initialisés par graine sont une troisième source, bien plus rare : l'échantillonneur appelle l'exponentielle et le logarithme de l'hôte dans ses branches rares, et environ un tirage sur un million diffère au dernier bit entre la construction native et la construction WASM.

Lorsqu'une sortie est discrète, un écart de dernière position n'est pas acceptable du tout, et le type de scénario est calculé avec src/portable_math.rs au lieu de la bibliothèque de l'hôte. Le type de scénario leo-navmsg est le premier : sa trame binaire est faite d'entiers transmis, et le même scénario a été codé une fois en trois trames différentes : dans une construction release, dans une construction debug de la même source, et dans le navigateur. C'est maintenant les mêmes octets dans les trois.

Pour cette raison, les tests de référence figée ne figent pas un seul hachage inter-plateformes de la sortie en virgule flottante — ce serait fragile et ferait échouer, à tort, des constructions correctes sur un autre OS. À la place :

  • tests/golden.rs fige chaque chiffre de mérite avec une tolérance relative de 1e-6 — quatre ordres de grandeur plus serrée que toute vraie régression (qui déplace une valeur de pourcents entiers) mais bien plus large que la gigue des bibliothèques mathématiques (libm) d'une plateforme à l'autre. Les champs bornés par la grille (secondes de holdover) et les champs exactement nuls sont figés exactement.
  • scenario_hash — un hachage du contenu des entrées — est indépendant de la plateforme et figé exactement.
  • tests/cross_platform_golden.rs fige un SHA-256 exact, versionné par scénario dans tests/golden/, sur la projection qui est identique d'une plateforme à l'autre : l'empreinte d'entrée plus la forme de sortie (noms de champs, imbrication, types de feuilles, longueurs de tableaux — fixés par l'arithmétique déterministe de la grille, jamais les valeurs en virgule flottante). Cela attrape exactement les régressions structurelles, tandis que les tolérances ci-dessus attrapent les régressions de valeurs.
  • scripts/check-reproducible.sh impose une sortie identique octet pour octet entre deux exécutions sur la même machine (la garantie de déterminisme).
  • Le job CI reproducibility-matrix exécute les quatre tests ci-dessus (cross_platform_golden, golden, determinism, sgp4_verification) sur ubuntu-latest, macos-latest et windows-latest, de sorte que la reproductibilité inter-plateformes est affirmée à chaque push — les références de forme et d'entrée exactement, la numérique à 1e-6 près, et les états SGP4 (Simplified General Perturbations 4) à 2e-5 km près — plutôt que de reposer sur un seul OS.

Si vous devez régénérer les nombres figés (par exemple après un changement de modèle intentionnel), exécutez chaque scénario de référence et copiez les valeurs FoM imprimées dans tests/golden.rs, puis notez le changement dans CHANGELOG.md.

Nomenclature logicielle (SBOM)#

scripts/gen-sbom.sh émet une SBOM CycloneDX 1,5 listant chaque crate livré dans un artefact kshana, avec sa version exacte, sa source et sa licence. C'est un générateur sans dépendance construit sur cargo metadata --locked (il fonctionne donc avec la seule chaîne d'outils), et il parcourt le graphe de résolution depuis le paquet kshana en suivant uniquement les dépendances normales et de construction. Les dépendances de développement (crates réservés aux tests tels que sgp4) sont exclues parce qu'aucun artefact ne les contient.

Le graphe est l'union des ensembles de fonctionnalités avec lesquels les artefacts livrés sont construits : la construction par défaut (bibliothèque et interface en ligne de commande (CLI)), --features python (la roue PyPI (Python Package Index), dont la chaîne pyo3 est la frontière d'interface avec le code étranger) et --features wasm (le paquet npm, qui porte cette même SBOM dans son archive). Les dépendances conditionnelles à la plateforme pour toutes les cibles sont incluses, puisque les roues sont livrées pour plusieurs systèmes d'exploitation et que le paquet npm cible WebAssembly. Un seul document couvre les trois artefacts, de sorte que pour l'un quelconque d'entre eux, c'est un sur-ensemble. Il liste actuellement 107 composants ; le décompte est figé dans tests/fixtures/reproducibility_software_assurance/. Le serveur autonome kshana-mcp a son propre manifeste et n'est pas décrit par cette SBOM.

La sortie est déterministe — le même ensemble de dépendances donne un document identique octet pour octet, y compris un numéro de série dérivé de la liste triée des paquets plutôt que d'un horodatage.

Le workflow de publication génère la SBOM (kshana-sbom.cdx.json) et la joint à chaque publication étiquetée ; le workflow de diffusion la livre aussi à côté des roues PyPI et dans le paquet npm.

Provenance de construction#

Le workflow de publication produit une attestation de provenance de construction SLSA (Supply-chain Levels for Software Artifacts) (actions/attest-build-provenance) couvrant chaque fichier qu'il joint à la publication GitHub : les binaires en ligne de commande de chaque plateforme, le binaire du serveur kshana-mcp, la SBOM, la synthèse de validation et SHA256SUMS. Un consommateur peut vérifier, avec gh attestation verify, que les artefacts ont été construits par le workflow de publication de ce dépôt à partir de cette source — comblant l'écart entre « voici un binaire » et « voici un binaire que je peux retracer jusqu'à sa source ». Par exemple, pour la SBOM de v0.28.0 :

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