Twierdzenia a rzeczywistość — rejestr nadmiernych twierdzeń
Niezależny audyt wcześniejszej wersji Kshana skatalogował czternaście nadmiernych twierdzeń (OC-0…OC-13): miejsc, w których powierzchnia publiczna (README, playground, etykiety wskaźników jakości (FoM), pakiety scenariuszy) opisywała możliwość mocniej, niż dostarczał kod. Ta strona jest rejestrem zamknięcia: każdy wiersz podaje pierwotne nadmierne twierdzenie, sposób jego rozwiązania i dowody. Występują dwa rodzaje rozwiązania:
- Wycofano twierdzenie — sformułowanie poprawiono tak, by odpowiadało kodowi (uczciwe przeformułowanie, bez zmiany możliwości). „Zero kodu = zero twierdzenia.”
- Zastąpione — rzeczywistą możliwość zbudowano i przetestowano później, więc mocne twierdzenie stało się trafne.
Strażnik regresji (tests/no_overclaims.rs) przy każdym przebiegu CI (ciągłej integracji) skanuje aktualne powierzchnie publiczne (README.md, docs/CAPABILITY.md, docs/GLOSSARY.md, web/capabilities.json, web/index.html, web/README.md oraz strony główne crates.io, PyPI (Python Package Index) i npm: README.crates.md, README.pypi.md, README.npm.md) i zgłasza błąd, jeśli którekolwiek z wycofanych gołych sformułowań nadmiernego twierdzenia pojawi się ponownie bez zastrzeżenia, więc wiersz nie może po cichu wrócić ze stanu GREEN.
Wszystkie czternaście wierszy jest GREEN.
| OC (nadmierne twierdzenie) | Pierwotne nadmierne twierdzenie | Rozwiązanie | Status | Dowody |
|---|---|---|---|---|
| OC-0 | „łączny estymator fuzji Kalmana” sugerował pojedynczy filtr z kowariancją krzyżową; kod uruchamiał dwa niezależne estymatory | Zastąpione — zbudowano prawdziwy filtr Kalmana zegara i pozycji, sprzężony kowariancją krzyżową | 🟢 | src/fusion/coupled.rs (7 testów, w tym zespół 100 prób sprzężony kontra rozłączony, który wymaga, by RMS (średnia kwadratowa) pozycji w wariancie sprzężonym był niższy niż 0,6× wariantu rozłączonego, a filtr sprzężony wygrał co najmniej 90 z 100 prób); CAPABILITY „Sensor fusion” → pełne |
| OC-1 | „RAIM (autonomiczny monitoring integralności odbiornika) wykrywania spoofingu wspomagany zegarem” sugerował wielosatelitarny detektor RAIM | Wycofano twierdzenie → Zastąpione — przeformułowano jako granicę wykrywalności spoofingu opartą na stabilności zegara; następnie pojawił się prawdziwy RAIM/ARAIM (HPL/VPL (HPL: poziomy poziom ochrony; VPL: pionowy poziom ochrony)) | 🟢 | src/raim.rs (30 testów — migawkowy + z separacją rozwiązań ARAIM, HPL/VPL, FDE (detekcja i wykluczanie uszkodzeń), diagramy Stanforda); docs/INTEGRITY.md |
| OC-2 | „demonstrator zagłuszania” bez żadnego kodu zagłuszania za nim | Zastąpione — zbudowano model zagłuszania oparty na bilansie łącza: J/S → efektywne C/N₀ → utrata synchronizacji | 🟢 | src/jamming.rs (10 testów); wiersz „Resilience” w README |
| OC-3 | „Pełny model szumu IMU (jednostki pomiaru inercjalnego) oparty na wariancji Allana dla triady IMU” — model był jednoosiowy | Wycofano twierdzenie → Zastąpione — przeformułowano jako budżet błędów 1-DOF (DOF: stopień swobody); następnie dostarczono trójosiowy INS (inercjalny system nawigacyjny) strapdown | 🟢 | src/inertial trójosiowy strapdown (orientacja kwaternionowa, mechanizacja NED (północ-wschód-dół), coning/sculling); ROADMAP „Inertial” |
| OC-4 | „Integracja hybrydowego PNT (pozycjonowanie, nawigacja i czas)” sugerowała sprzężony filtr GNSS/INS (GNSS: globalny system nawigacji satelitarnej); był to budżet błędów nawigowania zliczeniowego | Wycofano twierdzenie → Zastąpione — przeformułowano jako nawigowanie zliczeniowe z konfigurowalnym ponownym uchwyceniem; następnie dostarczono prawdziwą ścisło sprzężoną fuzję GNSS/INS | 🟢 | src/fusion/tightly_coupled17.rs (17-stanowy UKF (nieskentowany filtr Kalmana) z nawigowaniem zliczeniowym kwantowym CAI (CAI: interferometr zimnych atomów)); CAPABILITY „Sensor fusion” → pełne |
| OC-5 | „sprawdzone ok. 2%” sugerowało ścisłą, egzekwowaną bramkę | Wycofano twierdzenie — VALIDATION.md podaje egzekwowaną bramkę (20–25%, uśrednioną po ziarnach); „ok. 2%” oznaczało typową obserwację, a nie bramkę |
🟢 | docs/VALIDATION.md nagłówek „On tolerances” |
| OC-6 | „deterministyczny między platformami” bez zatwierdzonych dowodów | Wycofano twierdzenie — łańcuch narzędzi przypięty do dokładnego wydania; wzorcowe hasze dla każdego scenariusza zatwierdzone wraz z bramką odtwarzalności. (Identyczność bitowa między OS/arch (OS: system operacyjny) pozostaje otwartą pozycją, podaną uczciwie.) | 🟢 | rust-toolchain.toml (kanał 1.93.0); tests/golden.rs (wartości liczbowe do 1e-6); tests/cross_platform_golden.rs (hasz odcisku wejścia i kształtu każdego wyniku, uruchamiany w macierzy CI dla Linuksa, macOS i Windows); scripts/check-reproducible.sh |
| OC-7 | „hybrydowy kwantowo-klasyczny symulator PNT” sugerował fizykę kwantową od pierwszych zasad | Wycofano twierdzenie → Zastąpione — przeformułowano jako symulator odporności PNT używający modeli wydajności czujników kwantowych; następnie pojawiła się fizyka CAI Macha–Zehndera od pierwszych zasad | 🟢 | src/inertial/quantum_imu.rs (26 testów — faza Macha–Zehndera, szum projekcji 1/√(N·C²·T²), funkcja przenoszenia drgań, Coriolis + systematyki AC-Stark (AC: prąd przemienny)); docs/QUANTUM.md |
| OC-8 | wskaźnik jakości „Integrity Performance” sugerował lotniczą integralność HPL/VPL/RAIM | Wycofano twierdzenie + Zastąpione (warstwowo) — wskaźnik jakości scenariusza dla każdego przebiegu jest uczciwie oznaczony jako samospójność filtra (nie lotnicza integralność); prawdziwy ARAIM HPL/VPL jest pokazywany osobno, by obu nigdy nie mylić | 🟢 | src/fom.rs:80 (integrity: samospójność, z zastrzeżeniem); src/raim.rs + docs/INTEGRITY.md (prawdziwy ARAIM) |
| OC-9 | wskaźnik jakości Security przedstawiany jako zawsze znaczący, nawet bez ataku | Wycofano twierdzenie — wskaźnik jakości Security (1 − P_md) jest ujęty w kontekście detektora spoofingu i ma sens tylko wtedy, gdy skonfigurowano scenariusz ataku |
🟢 | wiersz „Resilience” w README; wskaźnik jakości Security jest zdefiniowany w punkcie specyfikacji szkodliwym operacyjnie |
| OC-10 | wskaźnik jakości „Positioning Performance” sugerował pełną dokładność w dziedzinie pozycji | Wycofano twierdzenie — oznaczono jako 1-DOF pos_rms_m dla pakietów inercjalnego/hybrydowego, wyraźnie nie jako 2-wymiarowy CEP/2DRMS (CEP: błąd kołowy prawdopodobny) ani dokładność ważona DOP (DOP: rozmycie dokładności) |
🟢 | tabela wskaźników jakości w README (wiersz „Positioning Performance”) |
| OC-11 | liczby wskaźników jakości inercjalnych odczytywane jako statystyki zespołu z pojedynczych ziaren | Wycofano twierdzenie — pojedynczy przebieg jest oznaczony monte_carlo: false; runs = N podaje średnią/rozrzut/przedział ufności bootstrap 95% |
🟢 | tabela wskaźników jakości w README; testy obwiedni pokrycia scenariuszy |
| OC-12 | scenariusz „konstelacji GPS (Global Positioning System) SGP4 (Simplified General Perturbations 4)” używał syntetycznych zastępczych TLE (zestawów elementów dwuliniowych) | Zastąpione — scenariusz osadza teraz prawdziwą migawkę Celestrak gps-ops z datą i ścisłymi sumami kontrolnymi |
🟢 | scenarios/orbit-sgp4-gps.toml (rzeczywiste gps-ops, strict_checksum); tests/scenario_coverage.rs |
| OC-13 | napis wersji w README rozjechał się z Cargo.toml |
Wycofano twierdzenie — bramka CI sprawdza, czy plakietka stanu w README zgadza się z Cargo.toml |
🟢 | scripts/check-version-sync.sh |
0,35: twierdzenia zachowane wąsko i jedna poprawka#
Funkcje 0,35 opisano z granicami podanymi obok twierdzenia, a te same strażniki (tests/no_overclaims.rs oraz strażnik sformułowań w tests/compliance_report.rs) skanują strony, które je opisują. Ta tabela nie jest częścią czternastowierszowego rejestru powyżej; dla nowych powierzchni zapisuje, co jest twierdzone, a co nie.
| Powierzchnia | Co jest twierdzone | Czego nie twierdzimy |
|---|---|---|
Wskaźnik zaufania do jednostki (receiver_trust, $PKSHT, bramka, Signal K, OpenCPN) |
wskaźnik 0-100 i przyczyny na podstawie własnego NMEA odbiornika, MODELLED | doradczo, nie jest to sprzęt nawigacyjny z zatwierdzeniem typu; wskaźnik dla jednego dziennika nie jest twierdzeniem o innych odbiornikach; nie zwiększa dokładności pozycji |
| Strumienie NMEA do szkolenia załóg | syntetyczny mostkowy NMEA ze scenariuszowymi zdarzeniami i dziennikiem instruktora | tylko tekst, bez wyjścia o częstotliwości radiowej; nigdy dla bieżących systemów nawigacyjnych jednostki; doradczo, nie jest to sprzęt nawigacyjny z zatwierdzeniem typu |
| Pakiety dowodowe | podpisany zapis techniczny, który można zweryfikować offline | nie jest opinią prawną; nie mówi, co spowodowało zdarzenie, kto za nie odpowiadał ani że dziennik pokazuje to, co odbiornik naprawdę odebrał |
| Mapa zakłóceń | zbiorcze komórki pogorszonej nawigacji z raportów na otwartych licencjach | nie jest prognozą; ekspozycja trasy to udział komórek, a nie ryzyko |
| Eksport dla test bench | ruch pojazdu i zdarzenia scenariusza w plikach, które może odczytać symulator laboratoryjny | nie jest zapisywany żaden sygnał; nie twierdzimy niczego o wydajności symulatora ani odbiornika |
| Mapowanie compliance do publicznych ram | które wiersze zestaw przebiegów wspiera dowodami (supports evidence for), z luką w każdym wierszu | nigdy że ramy są spełnione ani że produkt jest zatwierdzony; sama etykieta rodzaju nie jest dowodem |
Poprawka odnotowana w 0,35. Wcześniejsza wersja docs/RESILIENCE-CROSSWALK.md oraz komentarzy modułu odporności opisywała siedem „kategorii technik” ram DHS Resilient PNT Conformance Framework. Wersja 2,0 tych ram definiuje funkcje podstawowe (Prevent, Respond, Recover), poziomy od 0 do 4 i osiem ponumerowanych wymagań, a listy siedmiu kategorii nie ma. Siedem nazw podwskaźników, które emituje silnik oceny, to własne nazwy Kshana, i tabela powiązań teraz to mówi.
Jak wiersz pozostaje GREEN#
Mocne twierdzenia (OC-0/2/7/8 oraz zastąpione połowy OC-1/3/4/12) są GREEN, ponieważ możliwość jest dostarczona i przetestowana, a nie dlatego, że złagodzono sformułowanie. Wiersze wycofane z twierdzeń są GREEN, ponieważ aktualne sformułowanie odpowiada kodowi. Test strażnika czyni drugą kategorię egzekwowalną: jeśli wycofane sformułowanie nadmiernego twierdzenia wróci na powierzchnię publiczną, CI zaświeci się na czerwono. Zob. tests/no_overclaims.rs.