Кредо: «Жодної формули на віру. Жодної метафізичної галюцинації. Теорія → Археологія джерела → CAS/SMT доведення → Побітова перевірка в коді → Бенчмарк/тест → Фіксація аксіоми → Очищення середовища».
Статус: діючий (заміняє ескізи MVR-v1/v2 власника — узагальнені під реальні
потреби репозиторію). Перше застосування: цикли A–D (див. REGISTRY.md).
| # | Ескіз v1/v2 | Реальність v3 |
|---|---|---|
| 1 | «Ефемерні скрипти у scratch/ → видаляються» | Усі верифікатори багаторазові (воля власника): скрипт живе в git tools/verifiers/, викликається CLI-аргументами. «Одноразовий» = середовище (залежності), а не знання |
| 2 | Інструменти «створюються і видаляються» | Життєвий цикл станів: LOADED (встановлено) / STANDBY (скрипт у git, залежності не встановлені) / EVICTED (залежності видалено для економії RAM/диску). Завантаження = pip install, не «переписування скрипту» |
| 3 | QEMU/klee/valgrind/Coq у таблиці «наче є» | Чесний реєстр: що реально встановлено і перевірено (версії фіксуються), що — STANDBY з точною командою встановлення. Не імітуємо наявність того, чого нема |
| 4 | Абстрактні «бюджети контексту 128K» | Бюджети не постулюються, а вимірюються: розмір паспорту ≤ 4 КБ,scratch/ у .gitignore, повні виводи — у JSON на диску, у томи потрапляють лише числа |
| 5 | «Знайти формулу в архіві» | Фаза 0 обов'язкова: 299 першоджерел містять застарілі чернетки (приклад: критика лінійності PND відноситься до v6/v7; у v8 φ(a·b) +% ε·φ(a⊕b) з S-box x^254 лінійність знищена). Формула без звірки з актуальним кодом — гіпотеза, не аксіома |
Фаза 0 АРХЕОЛОГІЯ ДЖЕРЕЛА
джерело #NNN з 299 → актуальне / застаріле / перевизначене / скасоване;
git log/blame, звіркa з кодом; застаріле → документуємо еволюційний ланцюг
Фаза 1 ГІПОТЕЗА
точне формулювання (LaTeX), домен, аксіоми, прив'язка file#L у коді
Фаза 2 CAS/SMT ДОКАЗ
SymPy (символьні виведення), Z3 (бієктивність/колізії/інваріанти,
FP-теорія IEEE-754), NumPy/SciPy (чисельна валідація, Монте-Карло)
Фаза 3 ПОБІТОВА ЗВІРКА З КОДОМ
Rust: cargo test/asm; константи масок/таблиць звіряються з файлом;
розбіжність «модель ↔ код» фіксується як implementation gap
Фаза 4 ТЕСТ / БЕНЧМАРК
відтворюваний прогін, числа (не «швидко»); за потреби — новий тест у
кодовій базі, народжений верифікацією (improvement, не лише опис)
Фаза 5 ФІКСАЦІЯ АКСІОМИ
паспорт у том трактату (див. §5); theorem_id → verifier → commit → file#L
Фаза 6 ОЧИЩЕННЯ СЕРЕДОВИЩА
scratch/ вивід залишається поза git; залежності важких інструментів
можна EVICT; скрипт і паспорт лишаються в git назавжди
| Інструмент | Домен | Стан | Виклик |
|---|---|---|---|
python3 + numpy |
чисельна валідація, MC | LOADED (2.1.3) | python3 tools/verifiers/<v>.py |
python3 + sympy |
CAS: похідні, Z-перетворення | LOADED (1.14.0) | — // — |
python3 + z3-solver |
SMT: бієктивність, FP IEEE-754 | LOADED (5.1.0) | — // — |
python3 + scipy |
RK45-еталон для O(η)-збіжності дискретних схем | LOADED (1.14.1) | — // — |
python3 + qiskit |
квантов субстрат: DensityMatrix/expectation_value кросс-чек | LOADED (2.5.2) | — // — |
cargo test |
тести Rust-сторони | LOADED (rustc ≥1.87) | cargo test -p <crate> |
cargo bench / criterion |
бенчмарки | STANDBY | cargo bench --workspace |
cargo asm / objdump |
дизасемблювання | STANDBY | cargo install cargo-asm |
galois (python) |
поля GF(2^k), DDT/LAT | STANDBY — v3 обійшовся numpy-реалізацією GF(2⁸) | pip install galois |
zig test (poler-os) |
ядро PND v8 | НЕ ДОСТУПНИЙ у цьому репо — окремий репозиторій poler-os; код-грундінг PND — PENDING | — |
Правила: перед фазою 2 — python3 -c "import X" перевірка стану; встановлення
тільки потрібного; після циклу важкий пакет можна прибрати
(pip uninstall) — скрипти при цьому залишаються робочими (імпорти
лениво-перевіряються з чітким повідомленням, що встановити).
theorem_id (том.номер)
→ джерело #NNN (ENCYCLOPEDIA_299_SOURCES.md) [+ статус актуальності]
→ верифікатор tools/verifiers/<name>.py [-- режим]
→ JSON-паспорт scratch/passports/<cycle>.json (поза git)
→ числа + вердикт, вшиті у том трактату
→ код: файл#Lдіапазон (знімок на момент коміту)
→ commit-hash
Вердикти: AXIOM CONFIRMED (доказ + код-звірка збігаються) ·
CONFIRMED WITH CAVEATS (доведено в звуженому домені — домен зазначити) ·
REFUTED (контрприклад) · PENDING CODE GROUNDING (математика доведена,
коду нема в цьому репо).
## Паспорт інструментальної верифікації (MVR-v3)
- Теорема: II.1 · Джерело: #NNN [актуальне] · Цикл: B
- Інструменти: z3 5.1.0 (SMT FP), numpy 2.1.3 (побітово) · Команда: python3 tools/verifiers/verify_vg8_masks.py
- Доказ (SMT): <твердження, що саме доведено, unsat/такт>
- Чисельно: <вибірка, лічильники збігів/розбіжностей>
- Код: src/quantum/meta_compiler.rs#L83-L89, L151-L158, L897-L898 (commit 38a862a)
- Вердикт: CONFIRMED WITH CAVEATS — домен скінченних x; c=0 & x<0: +0.0 vs −0.0
(IEEE-754 рівність, біти різняться знаком нуля) — каveat зафіксовано тестом L1372
- Q.E.D. ■| Цикл | Том | Теорема | Верифікатор | Вердикт |
|---|---|---|---|---|
| B | II | II.1 (маски {-1,0,+1}) | verify_vg8_masks.py |
див. том |
| D | I | I.1 (ротор J=U−Uᵀ) | verify_rotor_norm.py |
див. том |
| C | III | III.1 (arcsin-MLE), III.2 (стиснення) | verify_rabitq_arcsin.py |
див. том |
| A | V | V.1/V.2 (PND: GF(2⁸), ARX) | verify_pnd_gf.py |
див. том |
| E | IV | IV.1 (IIR ⟺ Volterra/експ. слід) | verify_iir_z.py |
див. том |
| F | VII | VII.F.1–F.10 (єдене дискретне рівняння УДЕ) | verify_unified_discrete.py |
AXIOM CONFIRMED (10/10) |
Новий цикл = новий рядок + паспорт у томі. Жодна теорема не отримує
AXIOM CONFIRMED без виконаного скрипта з числами.