axiom-stack

This content is not available in your language yet.

Meta-repository и воспроизводимый reference pipeline для Autopoietic Proof-Carrying Computing.

Главный скачок v0.2

Reference path больше не доказывает abs перебором конечного диапазона. axiom-cegis получает контрпримеры от axiom-symbolic, пока не синтезирует программу, которая символически корректна для всех математических целых в поддерживаемом одномерном affine-фрагменте.

Запуск из этого репозитория при наличии соседних репозиториев:

python reference-v0.2.py

Скрипт также проверяет отказ после подмены proof-bound программы и запускает KV-эксперимент архитектурной эволюции.

Связанные исследования

Этот компонент входит в исследовательский проект Axiom. Все компоненты собраны по теме localzet-axiom. Основной язык документации — русский. Исследовательские результаты и ограничения не означают готовность к промышленному применению.

Компоненты и воспроизведение

components.json фиксирует проверенные коммиты всех 15 соседних компонентов. Этот метарепозиторий — шестнадцатый компонент. Зафиксированные версии воспроизводятся без привязки к путям конкретного компьютера:

git clone https://github.com/localzet/axiom-stack.git axiom/axiom-stack
cd axiom/axiom-stack
python3 bootstrap.py --directory ..
python3 reference-smoke.py
python3 reference-v0.2.py

Скрипт не меняет существующий репозиторий с другой версией или незакоммиченными файлами: используйте новую пустую папку для воспроизводимого эксперимента. Для Rust-компонентов выполняйте cargo test --locked --all-targets, для axiom-symbolic и axiom-cegis — python3 -m unittest discover -s tests -v в соответствующей папке. Формальные результаты проверяются командой lake build в axiom-formal на Lean из lean-toolchain.

Конечные обучающие примеры сами по себе не доказывают обобщение синтезированной программы. Символический backend поддерживает ограниченный одномерный аффинный фрагмент; другие конструкции должны отклоняться. Теоремы Lean проверяют модель, а соответствие VM этой модели ещё предстоит доказать. Эксперимент KV не является промышленной базой данных.

Карта исследований

CI метарепозитория проверяет зафиксированный набор целиком: Python reference/CEGIS/symbolic, сборку и тесты всех 11 Rust-компонентов с Clippy/rustfmt и формальную модель Lean. Зелёный CI подтверждает эти проверки, а не полноту proof coverage или production-готовность исследования.

rust-pipeline-smoke.py --bin-dir <cargo-target>/debug проверяет реальный Rust-компилятор, receipt gate и VM совместно с symbolic backend. Он проверяет обычные и граничные i64-значения, переполнение и отказ после подмены программы/receipt. Receipt gate пока проверяет согласованность полей и хешей, а не доверенность автора; недоверенные receipt требуют отдельного механизма верификации/аутентификации.

Исходный код · MIT