Metadata-Version: 2.4
Name: kern-gate
Version: 0.1.0
Summary: Kern Gate - Formal verification for game mechanics and contracts
Author: Kern Team
License: MIT
Keywords: verification,math,game,logic
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Requires-Python: >=3.10
Description-Content-Type: text/markdown
Requires-Dist: z3-solver

# Керн — контрактно-адресуемое программирование (рабочий набросок)

Керн — маленький язык с зависимыми типами, где единица публикации — не имя,
а **контракт**: тип-с-обещаниями, адресуемый хэшем своей канонической формы.
Реализация обязана предъявить свидетельство, и реестр честно различает его
ранг: `Assumed ⊏ Examples ⊏ PropTested ⊏ SMT ⊏ Proved`. Ядро — квантитативная
теория типов (мультипликативности 0/1/ω), режимы Tot/Par, Prop с
дефиниционной иррелевантностью; проверенное стирается: в рантайм уходит
только оплаченное.

Весь проект — прозрачный Python без магии: ~900 строк доверенного ядра,
остальное — инструменты вокруг него.

## Ворота для ИИ-кода — практическое применение

Главный практический инструмент комплекта — `gate.py`: вы не читаете код,
который написал ИИ, вы читаете вердикт ворот. Контракт (что функция обязана
делать) лежит в обычном python-файле, кандидата пишет любой ИИ, ворота
прогоняют его по лестнице: импорт → явные примеры → случайные свойства →
сверка с медленным-но-очевидным эталоном → полный перебор до границы.
Провал приходит с минимальным контрпримером; вердикт пишется в реестр
по хэшам содержимого, так что неизменные пары повторно не гоняются.

    python gate.py spec_median.py ai_draft.py    # черновик ИИ: пойман примерами
    python gate.py spec_median.py ai_sneaky.py   # коварный: пойман эталоном
    python gate.py spec_median.py ai_fixed.py    # исправленный: Исчерпание
    python gate.py --registry

Два рабочих цикла — по вашим силам.

Цикл для не-программиста (без единой строки вашего кода): скопируйте
`spec_vowels.py` — там только имя задачи и примеры «вход → ответ», которые
вы пишете сами, потому что понимаете смысл задачи. Попросите кандидатов у
двух-трёх РАЗНЫХ ИИ (или у одного в отдельных чатах) и устройте турнир:

    python gate.py spec_vowels.py ai_v1.py ai_v2.py ai_v3.py

Каждый пройдёт лестницу до ранга «Примеры», а затем консилиум столкнёт их
друг с другом на случайных входах, построенных по форме ваших примеров:
эталон не нужен — расхождение находится механически и ужимается до
минимального входа (в комплекте это одна заглавная буква «И», на которой
третий кандидат выдаёт 0 вместо 1). Заодно замеряется скорость. Согласие
всех — ещё не истина: если все ИИ поймут задачу одинаково неверно, консилиум
этого не увидит, поэтому ваши примеры — якорь; добавляйте туда каверзные
случаи (пустой вход, заглавные, отрицательные…) — можно спросить у ИИ,
какие каверзные случаи бывают, но правильные ответы к ним решаете вы.

Замкнутый цикл без ручных швов. Задание для ИИ ворота сочиняют сами из
вашей спеки: `python gate.py --brief спека.py` печатает готовый текст (и
кладёт в gate_brief.md) — скопируйте его в любой чат. Когда кандидат
проваливается, ворота пишут gate_report.md: минимальный вход, ожидание,
фактический ответ, обязательные примеры и просьба вернуть только
исправленный файл — вставьте отчёт в тот же чат и сохраните правку. При
расколе консилиума отчёт содержит голоса всех кандидатов и просит ИИ
рассудить по смыслу задачи. Круг «спека → задание → кандидат → вердикт →
отчёт → правка» замыкается без единой написанной вами строки кода.

Единая ведомость. `kernc.py` после успешного прогона записывает вердикты
ядра в тот же gate_registry.json — `python gate.py --registry` показывает
одну лестницу целиком: питоновские кандидаты с рангами от Черновика до
Исчерпания и рядом формально доказанные реализации Керна с рангом Proved,
все адресованные хэшами содержимого.

Цикл для умеющего немного программировать: скопируйте `spec_median.py` и
добавьте PROPERTIES, REFERENCE (эталон пишите самый глупый и очевидный,
скорость не важна) и EXHAUSTIVE — откроются верхние ступени лестницы.
Промпт для ИИ-кандидата — например такой:

    Напиши на Python функцию `median(xs)` (файл только с этой функцией,
    без main и без print): медиана списка чисел; для чётной длины —
    среднее двух центральных. Только код.

— сохраните ответ в файл и прогоните ворота. Ранги снизу вверх: Черновик,
Примеры, Свойства, Дифференциал, Исчерпание; вершина Proved достижима
только через ядро Керна. Честные границы: ворота исполняют кандидата
(отдельный процесс и лимит времени защищают от зависаний, но не от злого
умысла — прогоняйте лишь код, который и так собирались запустить), а
кривой контракт даст кривой вердикт: эталон и свойства — ваша часть сделки.

## Мост к вершине: Proved нажатием той же кнопки

Файл `.kern` — такой же кандидат для ворот, как `.py` и `.js`:

    python gate.py spec_double.py double.kern
    python gate.py spec_double.py ai_double.py double.kern

Раннер Керна прогоняет файл через ядро и приносит в рукопожатии «паспорт»:
ранги вызываемой функции и реализаций контрактов с их адресами. Если ядро
говорит Proved и лестница ворот пройдена целиком, итоговый ранг — Proved:
лестница здесь играет новую роль — она сверяет ДВЕ независимые
формализации замысла, спеку ворот и контракт ядра. Если же лестница
падает при доказанном контракте, ворота честно предупреждают: доказано не
то, что вы просили в спеке, — проверьте, что обе стороны об одном и том
же. Набросочные пределы: Керн-функции принимают лишь целые ≥ 0 (Nat), а
скорость через раннер — это интерпретатор плюс обмен между процессами.

## Любой язык программирования?

Да — по замыслу с любым, потому что ворота сравнивают поведение, а не
исходный текст: подали вход, сверили ответ; языку в этот протокол
просочиться неоткуда. Кандидаты на Python исполняются встроенно; для
остальных языков нужен «раннер» — переходник строк в тридцать. Первый уже
в комплекте: JavaScript (нужен установленный Node.js) — файл `.js` просто
передаётся воротам тем же способом, и питоновский эталон судит
JS-кандидата, а в турнире языки можно смешивать:

    python gate.py spec_median.py ai_median.js
    python gate.py spec_median.py ai_fixed.py ai_median.js

Задание для ИИ на другом языке: `python gate.py --brief спека.py js`.
Свой язык добавляется одним файлом-раннером по протоколу `runner_js.js`:
получить аргументами путь к файлу и имя функции; напечатать строку
{"ready":true}; затем на каждую JSON-строку аргументов отвечать строкой
{"ok":результат} или {"err":"текст"}; на конце входа — выйти. Для
компилируемых языков раннер сначала компилирует файл — ещё десяток строк.

Честные пределы: на машине должен стоять рантайм языка (node, компилятор…);
значения должны переживать JSON — числа, строки, списки да, экзотика типов
нет; дробные числа между языками сравниваются с допуском; замер скорости
через раннер включает накладные расходы обмена, поэтому сравнивать честно
лишь кандидатов на одном языке; лимит времени действует на фазу целиком.

## Требования

Python ≥ 3.10 (используется структурное сопоставление `match`).
Дополнительно и необязательно: `pip install z3-solver` — только для
SMT-моста (`kern_smt.py`, `demo_smt.py`, флаг `--smt`); без него всё
остальное работает, а SMT-тест аккуратно пропускается.

## Быстрый старт

Положите все файлы в одну папку и выполните:

    python3 run_tests.py            # прогон всех демонстраций с проверками
    python3 kernc.py example.kern --report
    python3 kernc.py --help

`run_tests.py` — регрессионный прогон: каждое демо обязано завершиться
успешно и напечатать свои ключевые маркеры (например `eval fib 10 = 55`).
`kernc.py` запускает ваш `.kern`-файл: загружает стандартную библиотеку
равенства (каждая лемма при этом доказывается ядром), исполняет декларации
по порядку, печатает по-русски, что принято и почему отказано. Флаг
`--report` показывает реестр доверия, `--smt` пытается поднять аксиомы
рангом Assumed до SMT решателем Z3.

## Ваш первый файл

Скопируйте `example.kern` и правьте его: там полный цикл — контракт `Double`,
очевидная реализация, быстрая реализация и её доказательство индукцией, после
чего обе стоят в реестре как `[Proved]`. В конце файла — предложение сломать
доказательство и посмотреть, как ядро объясняет отказ (с трассой «Где я был»).

Шпаргалка поверхности:

    def f : (x : Nat) -> Nat = \x. succ x        -- определение (ядро проверяет)
    def g : (x :0 A) -> (y :1 B) -> (z :w C) -> D -- мультипликативности 0/1/ω
    contract C = (n : Nat) -> { m : Nat | m == f n }   -- тип-с-обещанием (Σ+Prop)
    impl h : C = \n. (f n, refl)                 -- реализация ⊨ контракт
    assume ax : (n : Nat) -> P n                 -- аксиома (ранг Assumed)
    A ** B                                       -- Σ-тип;  (a, b) — пара
    a == b        refl                           -- равенство (Prop) и его интро
    elim n { zero => e | succ k ih => e2 }       -- рекурсия/индукция по Nat
    elim n return y. P { ... }                   -- …с мотивом (доказательства)
    data List (A : Type) : Type { nil | cons (a : A) (as : List A) }
    case xs { nil => e | cons a as ih => e2 }    -- разбор данных (ih после
    case h return z. P { ... }                   --  рекурсивных позиций)
    False    absurd e                            -- ⊥ и его элиминация
    rec f. e                                     -- общая рекурсия (режим Par)
    check refl : f 3 == 6                        -- проверка на стадии 0
    eval f 3                                     -- запуск стёртого кода
    -- комментарий до конца строки

Библиотека, доступная в каждом файле: `symN`, `transN`, `congN`, `cong_succ`,
`transportN`, `transportP` — леммы о равенстве на Nat (аргументы явные:
неявных аргументов в наброске нет, см. «Границы»).

## Что смотреть в демонстрациях

`demo_kern.py` — ядро без сахара: приёмка верного, отказ ложного, линейность,
стадии, α-инвариантный адрес контракта. `demo_surface.py` — поверхностный
язык, элаборация, реестр, диффер-тесты. `demo_smt.py` — мост в Z3: та же
задача рангами SMT/контрпример/капитуляция. `demo_proved.py` — вершина
решётки: индуктивные доказательства в поверхности, смерть аксиомы `add_comm`.
`demo_data.py` — схема индуктивов: позитивность, `Sum`, сильная рекурсия,
выведенная в языке, `fib` по двум предыдущим. `demo_reflect.py` — рефлексия:
обязательства уходят в Prop, в стёртом коде — ноль тегов, только арифметика.

## Python-API в пять строк

    from kern import Env
    from kern_store import Store
    from kern_lib import load_stdlib
    from kern_surface import run_program
    env = Env(); store = Store(env); load_stdlib(env)
    run_program(env, store, open("прога.kern").read()); store.report()

Дальше по вкусу: `kern_tools.erase / eeval / epretty / canon_hash` — стирание,
запуск, печать, адреса; `kern_smt.smt_certify_axiom / smt_check_candidate` —
решатель; `kern_build` — билдеры термов уровня ядра (так собрана kern_lib).

## Карта файлов

`kern.py` — доверенное ядро (TCB): термы, whnf, конверсия, `infer/check`
с векторами использования, схема индуктивов, `Env.define` — единственные
ворота в реестр. `kern_tools.py` — стирание, вычислитель стёртого,
канонизация и хэши. `kern_surface.py` — лексер, парсер, элаборатор,
драйвер `run_program`. `kern_store.py` — реестр доверия и ранги.
`kern_smt.py` — мост в Z3. `kern_build.py` — билдеры. `kern_lib.py` —
стандартная библиотека, доказываемая при загрузке. `kernc.py` — CLI,
`run_tests.py` — тесты, `example.kern` — стартовый шаблон.

## Неполадки

`AttributeError: module 'z3' has no attribute 'Int'` — в PyPI есть чужой
пакет с именем `z3`, затеняющий решатель. Лечение:
`python -m pip uninstall -y z3 z3-solver`, затем
`python -m pip install z3-solver`. Комплект различает самозванца сам:
тесты его пропускают с подсказкой, а `--smt` и demo_proved объясняют
причину; без решателя работоспособно всё, кроме SMT-ступени.
Если консоль Windows искажает символы вывода (Π, ⊨, ↯) — выполните
`chcp 65001` или задайте переменную окружения `PYTHONUTF8=1`.

## Границы наброска (честно)

Неявных аргументов нет — леммы вызываются со всеми аргументами. Индуктивы —
с параметрами, без индексированных семейств; позитивность первого порядка;
`elim return` — только по Nat. Универсумы без кумулятивности. `eval` печатает
числа и замыкания — устройств ввода-вывода нет. Ядро маленькое, но это
набросок для изучения идей, не производственная система: доверяйте ему ровно
настолько, насколько прочли его 911 строк.
