Tłumaczenie maszynowe, niezweryfikowane przez osobę, dla której polski jest językiem ojczystym. Wzorcem jest wersja angielska.

Walidacja i dowodyEdytuj na GitHubieŹródło: docs/REPRODUCIBILITY.md

Odtwarzalność i pochodzenie

Kshana jest zbudowany tak, by był odtwarzalny: te same dane wejściowe dają te same wyniki, a artefakty kompilacji można prześledzić do źródła, które je wytworzyło. Ten dokument mówi dokładnie, co jest gwarantowane, a co nie, i jak te gwarancje są egzekwowane.

Gwarancje determinizmu#

Silnik nie ma zegara ściennego, zależności od wątku wykonania ani niezasianej losowości. Każdy proces stochastyczny jest napędzany strumieniem ChaCha8Rng z kluczem w postaci seed scenariusza, losowanym w ustalonej kolejności. Konsekwencje:

Właściwość Gwarantowane Egzekwowane przez
Ten sam scenariusz, ta sama maszyna → identyczny co do bajta result.json Tak scripts/check-reproducible.sh (uruchamia scenariusz referencyjny dwukrotnie i porównuje SHA-256 (SHA: Secure Hash Algorithm))
Ten sam scenariusz → identyczne wskaźniki jakości pole po polu Tak, dla każdej platformy tests/golden.rs przypina każdy wskaźnik jakości (FoM) dla czterech scenariuszy referencyjnych
Skrót wejściowy scenariusza (scenario_hash) nie zależy od platformy Tak SHA-256 kanonicznego scenariusza adresowany treścią, przypięty w tests/golden.rs
Odcisk wejścia i kształt wyjścia identyczne na różnych systemach operacyjnych (OS) Tak tests/cross_platform_golden.rs przypina dokładny SHA-256 dla każdego scenariusza (dziesięć scenariuszy, po jednym pliku .sha256 w tests/golden/), sprawdzany w macierzy CI (continuous integration) dla 3-OS
Wartości wyjściowe zgadzają się na różnych systemach (ubuntu/macOS/Windows) Tak, do 1e-6 zadanie CI reproducibility-matrix uruchamia golden.rs (1e-6), sgp4_verification.rs (2e-5 km) i determinism.rs na wszystkich trzech systemach
Ramka komunikatu nawigacyjnego niskiej orbity okołoziemskiej (LEO) ma te same bajty na każdej platformie i w każdym profilu kompilacji, wraz z kompilacją WebAssembly (WASM) Tak src/portable_math.rs (każda funkcja przestępna i każda zmienna o rozkładzie normalnym rodzaju leo-navmsg przechodzi przez czysto rustowy pakiet libm); leo_navmsg::tests::the_encoded_frame_is_the_same_bytes_on_every_platform przypina całą ramkę bez bramki platformowej
Losowania indeksów z ziarna (próbkowanie bootstrap, tasowanie) są takie same na celach 32-bitowych i 64-bitowych Tak portable_math::uniform_index zawsze próbkuje jako u64; przypięte w portable_math::tests
Wszędzie ten sam zestaw narzędzi Tak rust-toolchain.toml przypina kanał; scripts/check-toolchain.sh przerywa kompilację przy rozbieżności; CI i wydanie przypinają tę samą wersję
Ten sam zestaw zależności Tak Cargo.lock jest zatwierdzony, a cargo metadata --locked służy do SBOM (software bill of materials)

Każdy przebieg z wiersza poleceń zapisuje też w raporcie zapis odtwarzalności (<scenario>.report.json i .report.html): wersję silnika, SHA-256 pliku scenariusza i dokumentu wynikowego, ziarno, platformę i dokładne polecenie, które tests/advanced_report_cli.rs uruchamia ponownie do wyniku identycznego co do bajta. Sam raport jest czystą funkcją przebiegu: dwa przebiegi scenarios/clock-holdover.toml zapisują ten sam report.json bajt w bajt. Zob. REPORTS.md.

Zastrzeżenie dotyczące różnych platform (i jak radzą sobie z nim wartości wzorcowe)#

Wyniki numeryczne są identyczne co do bitu na danej platformie, ale mogą się różnić o kilka ostatnich jednostek na ostatnim miejscu (ULP) między platformami. Przyczyną jest platformowa biblioteka matematyczna: sqrt, ln, exp i podobne nie muszą według IEEE-754 (IEEE: Institute of Electrical and Electronics Engineers) być poprawnie zaokrąglane, więc Linux (glibc, biblioteka GNU C), macOS i Windows mogą zwracać różny ostatni bit. W długim przebiegu te różnice rzędu ~1e-16 kumulują się do może ~1e-12 względnie.

Dwie rzeczy sprawiają, że różnica na ostatnim miejscu rośnie ponad swój początek i obie są zmierzone, a nie założone. Integrator adaptacyjny wybiera następny krok z oszacowania błędu przez pierwiastek piątego stopnia, więc jedna jednostka na ostatnim miejscu zmienia ciąg kroków i obie platformy zgadzają się wtedy tylko do tolerancji całkowania. Estymator iteracyjny (dopasowanie najmniejszych kwadratów, filtr wyznaczania orbity) może pójść inną drogą do zbieżności. Rodzaje zbudowane na jednym z nich mogą różnić się między platformami o więcej niż 1e-6 w poszczególnych polach; src/test_support.rs zapisuje ten sam reżim dla testów jednostkowych.

Profil kompilacji ma takie samo znaczenie na jednej maszynie. Zoptymalizowana kompilacja na macOS łączy sinus i cosinus jednego argumentu w jedno wywołanie połączonej procedury systemowej, której sinus różni się od samotnego sin na ostatnim bicie dla 379 z 200 000 argumentów; kompilacja niezoptymalizowana wykonuje dwa wywołania. Zmierzono na aarch64 macOS dla 138 plików scenariuszy: kompilacja debug i release jednego źródła dają dokumenty wynikowe identyczne co do bajta dla 102. Pozostałe 36 różnią się na ostatnich miejscach: 28 w granicach 1e-6, jeden (leo-ppp-convergence) o 2.8e-6, a siedem kampanii tylko w skrótach swoich przebiegów składowych; żaden nie różni się etykietą, liczbą ani werdyktem. Gwarancja identyczności co do bajta powyżej dotyczy więc jednej kompilacji: tego samego pliku binarnego dwukrotnie.

Losowania rozkładu normalnego z ziarna są trzecim, znacznie rzadszym źródłem: próbnik wywołuje funkcje wykładniczą i logarytm hosta w swoich rzadkich gałęziach, a około jedno losowanie na milion różni się ostatnim bitem między kompilacją natywną a WASM.

Tam, gdzie wynik jest dyskretny, różnica na ostatnim miejscu nie jest w ogóle dopuszczalna, a dany rodzaj jest obliczany za pomocą src/portable_math.rs zamiast biblioteki hosta. Rodzaj leo-navmsg jest pierwszym z nich: jego ramka binarna to przesyłane liczby całkowite, a ten sam scenariusz kodował się kiedyś do trzech różnych ramek: w kompilacji release, w kompilacji debug tego samego kodu źródłowego i w przeglądarce. Teraz są to w tych trzech przypadkach te same bajty.

Z tego powodu testy złotych wzorców (golden) nie przypinają jednego, wspólnego dla platform skrótu wyniku zmiennoprzecinkowego: byłoby to kruche i powodowałoby odrzucanie poprawnych kompilacji na innym systemie operacyjnym. Zamiast tego:

  • tests/golden.rs przypina każdy wskaźnik jakości z tolerancją względną 1e-6, czyli o cztery rzędy wielkości ciaśniejszą niż jakakolwiek rzeczywista regresja (która zmienia wartość o całe procenty), a zarazem znacznie luźniejszą niż wahania międzyplatformowej biblioteki matematycznej (libm). Pola ograniczone siatką (sekundy holdover) i pola dokładnie równe zeru są przypinane dokładnie.
  • scenario_hash, czyli skrót zawartości danych wejściowych, nie zależy od platformy i jest przypinany dokładnie.
  • tests/cross_platform_golden.rs przypina dokładny skrót SHA-256, zapisany dla każdego scenariusza w tests/golden/, z projekcji, która jest identyczna na wszystkich platformach: odcisk danych wejściowych oraz kształt wyniku (nazwy pól, zagnieżdżenie, typy liści, długości tablic, wyznaczane deterministyczną arytmetyką siatki, nigdy wartości zmiennoprzecinkowe). Wychwytuje to dokładnie regresje strukturalne, natomiast przypięte wyżej tolerancje wychwytują regresje wartości.
  • scripts/check-reproducible.sh wymusza identyczność bajt po bajcie wyniku z dwóch przebiegów na tej samej maszynie (gwarancja determinizmu).
  • Zadanie CI reproducibility-matrix uruchamia cztery powyższe testy (cross_platform_golden, golden, determinism, sgp4_verification) na ubuntu-latest, macos-latest i windows-latest, dzięki czemu odtwarzalność międzyplatformowa jest sprawdzana przy każdym wypchnięciu zmian: złote wzorce kształtu i danych wejściowych dokładnie, wartości liczbowe z dokładnością do 1e-6, a stany SGP4 (Simplified General Perturbations 4) do 2e-5 km, zamiast polegać na jednym systemie operacyjnym.

Jeśli trzeba ponownie wygenerować przypięte liczby (na przykład po zamierzonej zmianie modelu), uruchom każdy scenariusz referencyjny i skopiuj wypisane wartości wskaźników jakości do tests/golden.rs, a następnie odnotuj zmianę w CHANGELOG.md.

Wykaz składników oprogramowania (SBOM)#

scripts/gen-sbom.sh generuje wykaz SBOM w formacie CycloneDX 1,5, w którym znajduje się każdy crate dostarczany w artefakcie kshana, z dokładną wersją, źródłem i licencją. Jest to generator bez zależności, zbudowany na cargo metadata --locked (działa więc z samym zestawem narzędzi), który przechodzi graf rozwiązanych zależności od pakietu kshana, uwzględniając wyłącznie zwykłe zależności i zależności budowania. Zależności deweloperskie (crate'y tylko do testów, takie jak sgp4) są pomijane, ponieważ żaden artefakt ich nie zawiera.

Graf jest sumą zestawów funkcji, z którymi budowane są dostarczane artefakty: kompilacji domyślnej (biblioteka i CLI (interfejs wiersza poleceń)), --features python (pakiet wheel w PyPI (Python Package Index), w którym łańcuch pyo3 stanowi granicę interfejsu obcych funkcji) oraz --features wasm (pakiet npm, który nosi ten sam SBOM w swoim archiwum tarball). Uwzględnione są zależności warunkowe względem platformy dla każdego celu, ponieważ pakiety wheel są dostarczane dla kilku systemów operacyjnych, a pakiet npm jest przeznaczony dla WebAssembly. Jeden dokument obejmuje wszystkie trzy artefakty, więc dla każdego z osobna jest on nadzbiorem. Obecnie wymienia 107 składników; liczba ta jest przypięta w tests/fixtures/reproducibility_software_assurance/. Samodzielny serwer kshana-mcp ma własny manifest i ten SBOM go nie opisuje.

Wynik jest deterministyczny: ten sam zbiór zależności daje identyczny bajt po bajcie dokument, w tym numer seryjny wyprowadzony z posortowanej listy pakietów, a nie ze znacznika czasu.

Przepływ pracy wydania generuje SBOM (kshana-sbom.cdx.json) i dołącza go do każdego otagowanego wydania; przepływ publikacji dostarcza go także obok pakietów wheel w PyPI oraz wewnątrz pakietu npm.

Pochodzenie kompilacji#

Przepływ pracy wydania tworzy poświadczenie pochodzenia kompilacji SLSA (Supply-chain Levels for Software Artifacts) (actions/attest-build-provenance), obejmujące każdy plik dołączony do wydania na GitHubie: pliki binarne wiersza poleceń dla każdej platformy, plik binarny serwera kshana-mcp, SBOM, podsumowanie walidacji i SHA256SUMS. Odbiorca może za pomocą gh attestation verify sprawdzić, że artefakty zostały zbudowane przez przepływ pracy wydania tego repozytorium z tego kodu źródłowego, co zamyka lukę między „oto plik binarny” a „oto plik binarny, który mogę wyśledzić do jego źródła”. Na przykład dla SBOM wersji 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