Машинний переклад, не перевірений носієм мови. Еталоном є англійська версія.

Валідація та доказиРедагувати на GitHubДжерело: docs/REPRODUCIBILITY.md

Відтворюваність і походження

Kshana побудовано відтворюваною: ті самі входи дають ті самі результати, а артефакти збірки можна простежити до джерела, яке їх створило. Цей документ точно визначає, що гарантовано, що ні і як ці гарантії забезпечуються.

Гарантії детермінізму#

Рушій не має залежності від настінного годинника, від потоку виконання та від нерозсіяної випадковості. Кожен стохастичний процес керується потоком ChaCha8Rng, ключем якого є seed сценарію, і береться у фіксованому порядку. Наслідки:

Властивість Гарантовано Забезпечується через
Той самий сценарій, та сама машина → побайтово ідентичний result.json Так scripts/check-reproducible.sh (двічі запускає еталонний сценарій і порівнює SHA-256 (SHA: Secure Hash Algorithm))
Той самий сценарій → ідентичні показники якості поле за полем Так, на кожній платформі tests/golden.rs фіксує кожен показник якості (FoM) для чотирьох еталонних сценаріїв
Хеш входу сценарію (scenario_hash) не залежить від платформи Так SHA-256 канонічного сценарію за вмістом, зафіксований у tests/golden.rs
Відбиток входу + форма виходу ідентичні в різних ОС (операційних системах) Так tests/cross_platform_golden.rs фіксує точний SHA-256 для кожного сценарію (десять сценаріїв, по одному файлу .sha256 у tests/golden/), що перевіряється на матриці CI (безперервної інтеграції) з 3 ОС
Значення виходу збігаються в різних ОС (ubuntu/macOS/Windows) Так, з точністю до 1e-6 завдання CI reproducibility-matrix запускає golden.rs (1e-6), sgp4_verification.rs (2e-5 км) і determinism.rs на всіх трьох ОС
Кадр навігаційного повідомлення низької навколоземної орбіти (LEO) — ті самі байти на кожній платформі та в кожному профілі збірки, зокрема у збірці WebAssembly (WASM) Так src/portable_math.rs (кожна трансцендентна функція та кожне нормальне відхилення виду leo-navmsg проходять через крейт libm на чистому Rust); 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 файлу сценарію та документа результату, зерно (seed), платформу й точну команду, яку tests/advanced_report_cli.rs перезапускає до побайтово ідентичного результату. Сам звіт є чистою функцією запуску: два запуски scenarios/clock-holdover.toml записують той самий report.json байт у байт. Див. REPORTS.md.

Застереження щодо різних платформ (і як із ним поводяться еталонні значення)#

Числові результати побітово ідентичні на заданій платформі, але можуть відрізнятися в останніх кількох одиницях молодшого розряду (ULP) між платформами. Причина — математична бібліотека платформи: 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 зливає синус і косинус одного аргумента в один виклик комбінованої підпрограми системи, синус якої відрізняється від окремого sin в останньому біті для 379 із 200 000 аргументів; неоптимізована збірка робить два виклики. За вимірюванням на aarch64 macOS на 138 файлах сценаріїв, налагоджувальна та релізна збірки одного джерела дають побайтово ідентичні документи результату для 102. Решта 36 відрізняються в останніх розрядах: 28 у межах 1e-6, один (leo-ppp-convergence) на 2.8e-6, а сім кампаній лише в дайджестах своїх запусків-членів; жоден не відрізняється в мітці, кількості чи вердикті. Тому гарантія побайтової ідентичності вище стосується однієї збірки: того самого бінарного файлу двічі.

Розсіяні нормальні вибірки — третє, значно рідше джерело: семплер викликає хостові експоненту й логарифм у своїх рідкісних гілках, і приблизно одна вибірка з мільйона відрізняється в останньому біті між нативною збіркою та збіркою WASM.

Там, де вихід дискретний, різниця в останньому розряді взагалі неприйнятна, і вид обчислюється за допомогою src/portable_math.rs замість бібліотеки хоста. Вид leo-navmsg — перший такий: його двійковий кадр складається з переданих цілих чисел, і той самий сценарій колись кодувався в три різні кадри: у релізній збірці, в налагоджувальній збірці того самого джерела та в браузері. Тепер це ті самі байти в усіх трьох.

Через це тести еталонних значень не фіксують єдиний міжплатформний хеш виходу з плаваючою комою: він був би крихким і чесно завалював би правильні збірки на іншій ОС. Натомість:

  • tests/golden.rs фіксує кожен показник якості з відносним допуском 1e-6 — на чотири порядки жорсткішим за будь-яку реальну регресію (яка зсуває значення на цілі відсотки), але набагато м'якшим за міжплатформний шум математичної бібліотеки (libm). Поля, обмежені сіткою (секунди holdover), і поля з точним нулем фіксуються точно.
  • scenario_hash — хеш вмісту входів — не залежить від платформи й фіксується точно.
  • tests/cross_platform_golden.rs фіксує точний SHA-256, закомічений для кожного сценарію в tests/golden/, для проєкції, що є ідентичною на різних платформах: відбиток входу плюс форма виходу (назви полів, вкладеність, типи листків, довжини масивів — визначені детермінованою арифметикою сітки, а не значеннями з плаваючою комою). Це точно виявляє структурні регресії, тоді як допуски вище виявляють регресії значень.
  • scripts/check-reproducible.sh забезпечує побайтово ідентичний вихід у двох запусках на тій самій машині (гарантія детермінізму).
  • Завдання CI reproducibility-matrix запускає чотири тести вище (cross_platform_golden, golden, determinism, sgp4_verification) на ubuntu-latest, macos-latest і windows-latest, тож міжплатформна відтворюваність перевіряється під час кожного пушу — еталонні форми й входи точно, числа з точністю до 1e-6, а стани SGP4 (Simplified General Perturbations 4) з точністю до 2e-5 км — замість того, щоб покладатися на одну ОС.

Якщо потрібно перегенерувати зафіксовані числа (наприклад, після навмисної зміни моделі), запустіть кожен еталонний сценарій і скопіюйте надруковані значення FoM у tests/golden.rs, а потім зазначте зміну в CHANGELOG.md.

Специфікація складників програмного забезпечення (SBOM)#

scripts/gen-sbom.sh створює SBOM CycloneDX 1,5, що перелічує кожен крейт, який постачається в артефакті kshana, з його точною версією, джерелом і ліцензією. Це генератор без залежностей, побудований на cargo metadata --locked (тож він працює лише з інструментарієм), і він обходить граф розв'язання від пакета kshana лише через звичайні залежності та залежності збірки. Залежності розробки (крейти лише для тестів, як-от sgp4) виключено, бо жоден артефакт їх не містить.

Граф є об'єднанням наборів можливостей, з якими збираються постачані артефакти: типова збірка (бібліотека та інтерфейс командного рядка (CLI)), --features python (колесо PyPI (Python Package Index), чий ланцюг pyo3 є його межею зовнішніх функцій) і --features wasm (пакет npm, який несе цей самий SBOM усередині свого тарбола). Залежності, обумовлені платформою, для кожної цілі включено, оскільки колеса постачаються для кількох операційних систем, а пакет npm націлений на WebAssembly. Один документ охоплює всі три артефакти, тож для будь-якого окремого він є надмножиною. Наразі він перелічує 107 компонентів; це число зафіксовано в tests/fixtures/reproducibility_software_assurance/. Окремий сервер kshana-mcp має власний маніфест і цим SBOM не описується.

Вихід детермінований: той самий набір залежностей дає побайтово ідентичний документ, зокрема серійний номер, виведений із відсортованого списку пакетів, а не з позначки часу.

Робочий процес релізу генерує SBOM (kshana-sbom.cdx.json) і додає його до кожного позначеного тегом релізу; робочий процес публікації також постачає його поруч із колесами PyPI та всередині пакета npm.

Походження збірки#

Робочий процес релізу створює атестацію походження збірки SLSA (Supply-chain Levels for Software Artifacts) (actions/attest-build-provenance), що охоплює кожен файл, який він додає до GitHub Release: бінарні файли командного рядка для кожної платформи, бінарний файл сервера kshana-mcp, SBOM, підсумок валідації та SHA256SUMS. Споживач може за допомогою gh attestation verify перевірити, що артефакти зібрано робочим процесом релізу цього репозиторію з цього джерела, — закриваючи розрив між «ось бінарний файл» і «ось бінарний файл, який я можу простежити до його джерела». Наприклад, для SBOM версії 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