Metadata-Version: 2.4
Name: kern-gate
Version: 0.1.1
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

# Kern Gate — Contract-Addressed Programming (Working Draft)

[Russian version below](#керн--контрактно-адресуемое-программирование-рабочий-набросок)

Kern is a small dependently-typed language where the unit of publication is not a name, but a **contract**: a type-with-promises addressed by the hash of its canonical form. The implementation must present evidence, and the registry honestly distinguishes its rank: `Assumed ⊏ Examples ⊏ PropTested ⊏ SMT ⊏ Proved`. The core is a quantitative type theory (multiplicities 0/1/ω), Tot/Par modes, Prop with definitional irrelevance; the proven code is erased: only the paid code goes to runtime.

The whole project is transparent Python with no magic: ~900 lines of trusted core, the rest are tools around it.

## The Gate for AI Code — Practical Application

The main practical tool of the kit is `gate.py`: you don't read the code written by the AI, you read the verdict of the gate. The contract (what the function must do) lies in a regular python file, the candidate is written by any AI, and the gate runs it up the ladder: import → explicit examples → random properties → checking against a slow-but-obvious reference → exhaustive search to the boundary. Failure comes with a minimal counterexample; the verdict is written to the registry by content hashes, so unchanged pairs are not re-run.

    python gate.py spec_median.py ai_draft.py    # AI draft: caught by examples
    python gate.py spec_median.py ai_sneaky.py   # Sneaky: caught by reference
    python gate.py spec_median.py ai_fixed.py    # Fixed: Exhaustive
    python gate.py --registry

Two workflows — according to your abilities.

Workflow for a non-programmer (without a single line of your code): copy `spec_vowels.py` — it only contains the task name and "input → answer" examples, which you write yourself because you understand the meaning of the task. Ask for candidates from two or three DIFFERENT AIs (or from one in separate chats) and arrange a tournament:

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

Each will pass the ladder to the "Examples" rank, and then the council will pit them against each other on random inputs built in the shape of your examples: no reference is needed — the discrepancy is found mechanically and shrunk to a minimal input. Speed is also measured. The agreement of all is not yet the truth: if all AIs misunderstand the task equally incorrectly, the council will not see it, so your examples are the anchor; add tricky cases there (empty input, uppercase, negative...) — you can ask the AI what the tricky cases are, but you decide the correct answers to them.

Closed loop without manual seams. The gate itself composes the task for the AI from your spec: `python gate.py --brief spec.py` prints the finished text (and puts it in gate_brief.md) — copy it to any chat. When the candidate fails, the gate writes gate_report.md: minimal input, expectation, actual answer, mandatory examples, and a request to return only the fixed file — paste the report into the same chat and save the edit. When the council splits, the report contains the votes of all candidates and asks the AI to judge by the meaning of the task. The cycle "spec → task → candidate → verdict → report → edit" closes without a single line of code written by you.

Unified registry. `kernc.py` after a successful run writes the core verdicts to the same gate_registry.json — `python gate.py --registry` shows one ladder as a whole: Python candidates with ranks from Draft to Exhaustive and next to them formally proven Kern implementations with the Proved rank, all addressed by content hashes.

Workflow for someone who can program a bit: copy `spec_median.py` and add PROPERTIES, REFERENCE (write the stupidest and most obvious reference, speed doesn't matter) and EXHAUSTIVE — the upper steps of the ladder will open. A prompt for the AI candidate — for example like this:

    Write a function `median(xs)` in Python (a file with only this function, without main and without print): the median of a list of numbers; for even length — the average of the two central ones. Only code.

— save the answer to a file and run the gate. Ranks from bottom to top: Draft, Examples, Properties, Differential, Exhaustive; the Proved peak is reachable only through the Kern core. Honest boundaries: the gate executes the candidate (a separate process and time limit protect against hangs, but not against malicious intent — only run code that you were going to run anyway), and a crooked contract will give a crooked verdict: the reference and properties are your part of the deal.

## Bridge to the Peak: Proved by pressing the same button

A `.kern` file is the same candidate for the gate as `.py` and `.js`:

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

The Kern runner passes the file through the core and brings a "passport" in a handshake: the ranks of the called function and the implementations of the contracts with their addresses. If the core says Proved and the gate ladder is completed entirely, the final rank is Proved: the ladder plays a new role here — it verifies TWO independent formalizations of the intent, the gate spec and the core contract. If the ladder falls with a proven contract, the gate honestly warns: what is proven is not what you asked for in the spec — check that both sides are about the same thing. Draft limits: Kern functions only accept integers ≥ 0 (Nat), and the speed through the runner is an interpreter plus communication between processes.

## Any programming language?

Yes — by design with any, because the gate compares behavior, not source text: submitted input, checked answer; there is nowhere for the language to leak into this protocol. Python candidates are executed natively; for other languages, a "runner" is needed — an adapter of about thirty lines. The first one is already included: JavaScript (requires installed Node.js) — a `.js` file is simply passed to the gate in the same way, and the Python reference judges the JS candidate, and languages can be mixed in the tournament:

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

Task for an AI in another language: `python gate.py --brief spec.py js`. A new language is added with a single runner file following the `runner_js.js` protocol: receive the file path and function name as arguments; print the string {"ready":true}; then answer each JSON string of arguments with the string {"ok":result} or {"err":"text"}; exit at the end of the input. For compiled languages, the runner first compiles the file — another dozen lines.

Honest limits: the machine must have the language runtime installed (node, compiler...); values must survive JSON — numbers, strings, lists yes, exotic types no; fractional numbers between languages are compared with a tolerance; speed measurement through the runner includes communication overhead, so it's fair to compare only candidates in the same language; the time limit applies to the phase as a whole.

## Requirements

Python ≥ 3.10 (uses structural pattern matching `match`).
Additional and optional: `pip install z3-solver` — only for the SMT bridge (`kern_smt.py`, `demo_smt.py`, `--smt` flag); without it, everything else works, and the SMT test is neatly skipped.

## Quick Start

Put all files in one folder and run:

    python3 run_tests.py            # run all demonstrations with checks
    python3 kernc.py example.kern --report
    python3 kernc.py --help

`run_tests.py` — regression run: each demo must complete successfully and print its key markers (e.g., `eval fib 10 = 55`). `kernc.py` runs your `.kern` file: loads the standard equality library (each lemma is proven by the core in the process), executes declarations in order, prints in Russian what is accepted and why it was rejected. The `--report` flag shows the trust registry, `--smt` tries to raise axioms with the Assumed rank to SMT with the Z3 solver.

## Your first file

Copy `example.kern` and edit it: there is a full cycle there — the `Double` contract, obvious implementation, fast implementation and its proof by induction, after which both stand in the registry as `[Proved]`. At the end of the file — a proposal to break the proof and see how the core explains the rejection (with the "Where I was" trace).

Surface cheat sheet:

    def f : (x : Nat) -> Nat = \x. succ x        -- definition (core checks)
    def g : (x :0 A) -> (y :1 B) -> (z :w C) -> D -- multiplicities 0/1/ω
    contract C = (n : Nat) -> { m : Nat | m == f n }   -- type-with-promise (Σ+Prop)
    impl h : C = \n. (f n, refl)                 -- implementation ⊨ contract
    assume ax : (n : Nat) -> P n                 -- axiom (Assumed rank)
    A ** B                                       -- Σ-type; (a, b) — pair
    a == b        refl                           -- equality (Prop) and its intro
    elim n { zero => e | succ k ih => e2 }       -- recursion/induction on Nat
    elim n return y. P { ... }                   -- …with a motive (for proofs)
    data List (A : Type) : Type { nil | cons (a : A) (as : List A) }
    case xs { nil => e | cons a as ih => e2 }    -- data matching (ih after rec. pos.)
    case h return z. P { ... }                   
    False    absurd e                            -- ⊥ and its elimination
    rec f. e                                     -- general recursion (Par mode)
    check refl : f 3 == 6                        -- check at phase 0
    eval f 3                                     -- run erased code
    -- comment to the end of line

Library available in every file: `symN`, `transN`, `congN`, `cong_succ`, `transportN`, `transportP` — equality lemmas on Nat (arguments are explicit: there are no implicit arguments in the draft, see "Boundaries").

## What to see in demonstrations

`demo_kern.py` — core without sugar: accepting the true, rejecting the false, linearity, stages, α-invariant contract address. `demo_surface.py` — surface language, elaboration, registry, differ-tests. `demo_smt.py` — bridge to Z3: the same task with SMT/counterexample/capitulation ranks. `demo_proved.py` — peak of the lattice: inductive proofs in the surface, death of the `add_comm` axiom. `demo_data.py` — inductive scheme: positivity, `Sum`, strong recursion derived in the language, `fib` by the previous two. `demo_reflect.py` — reflection: obligations go to Prop, in the erased code — zero tags, only arithmetic.

## Python API in five lines

    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("prog.kern").read()); store.report()

Further to taste: `kern_tools.erase / eeval / epretty / canon_hash` — erasure, erased evaluator, printing, addresses; `kern_smt.smt_certify_axiom / smt_check_candidate` — solver; `kern_build` — core-level term builders (how kern_lib is built).

## File map

`kern.py` — trusted core (TCB): terms, whnf, conversion, `infer/check` with usage vectors, inductive scheme, `Env.define` — the only gate to the registry. `kern_tools.py` — erasure, erased evaluator, canonization and hashes. `kern_surface.py` — lexer, parser, elaborator, `run_program` driver. `kern_store.py` — trust registry and ranks. `kern_smt.py` — bridge to Z3. `kern_build.py` — builders. `kern_lib.py` — standard library, proven upon loading. `kernc.py` — CLI, `run_tests.py` — tests, `example.kern` — starter template.

## Troubleshooting

`AttributeError: module 'z3' has no attribute 'Int'` — there is someone else's package with the name `z3` in PyPI shadowing the solver. Cure: `python -m pip uninstall -y z3 z3-solver`, then `python -m pip install z3-solver`. The kit distinguishes the impostor itself: tests skip it with a hint, and `--smt` and demo_proved explain the reason; without the solver, everything works except the SMT step.
If the Windows console distorts output characters (Π, ⊨, ↯) — execute `chcp 65001` or set the environment variable `PYTHONUTF8=1`.

## Draft boundaries (honestly)

No implicit arguments — lemmas are called with all arguments. Inductives — with parameters, without indexed families; first-order positivity; `elim return` — only on Nat. Universes without cumulativity. `eval` prints numbers and closures — there are no I/O devices. The core is small, but it's a draft for exploring ideas, not a production system: trust it exactly as much as you've read its 911 lines.

---

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

Керн — маленький язык с зависимыми типами, где единица публикации — не имя, а **контракт**: тип-с-обещаниями, адресуемый хэшем своей канонической формы. Реализация обязана предъявить свидетельство, и реестр честно различает его ранг: `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 строк.
