Skip to content

KERN v2.5.0 — Native LIA Solver, 120 Lean 4 Theorems, 7-Language X-Ray & Formal Trust Scorecard

Choose a tag to compare

View all tags
@newmathphys newmathphys released this 19 Oct 18:32
· 36 commits to main since this release
v2.5.0
54439ee

KERN v2.5.0 — release notes

Дата: 2026-10-19 · Ветка: v2.5-dev → main · Предыдущий релиз: v2.4.0 (28e6bb9)

Это не «ещё один линтер». Каждое заявление ниже имеет машинное свидетельство:
либо trusted: 0 | holes: 0 в пруф-чекере, либо прогон, который способен упасть
(can-fail), либо теорема Lean 4. Числа, которые измерить не удалось, помечены
как неизмеренные — их здесь нет.

Что изменилось: v2.4.0 → v2.5.0

Метрика v2.4.0 v2.5.0
Тесты ядра Zig 299 401 (393 passed + 8 skipped, 0 failed)
KERN-Next 38 53
Каталог тестов 337 424
Теоремы Lean 4 42 120 в 8 файлах (0 errors, 0 sorry)
Мутации (канон. срез) 95.0 % (38/40) 100.0 % (40/40)
Мутации (полный обстрел) не проводился 1225 / 1225 = 100.0 % (20 файлов)
Can-fail 82/82 CHECK 125/125 CHECK, 141 не-вакуумных кейсов, 0 вакуумных
Подделки доказательств 30/30 40/40 отклонены (QF_LIA, QF_S, IEEE-754)
Языки контрактов 4 7 (+ .ts, .js, .go)
MCP-инструменты 5 8 (+ xray, verify_action, rlvr_reward) + аннотации
WebAssembly нет kernc.wasm (86 953 Б; 5 функций kern_wasm_*, включая verify_proof; всего 7 записей экспорта с memory/__stack_pointer)
Кросс-архитектура 240 (устаревший лог) 393 passed / 8 skipped / 0 failed (ARM64 + PPC64 BE)

Восемь эшелонов (40 пунктов)

  1. Ядро (L3–L4) — встроенный решатель Фурье — Моцкина (builtin_lia.zig,
    100 систем против Z3, 0 расхождений), проверка SAT-моделей внутри Zig,
    musl abs.c переведён из SKIP в PROVEN (51 шаг, trusted: 0), защита
    от let-бомбы, минимизация контрпримеров, 64-битный код допуска, капсула Z3
    (RLIMIT_FSIZE = 0, очистка окружения).
  2. Контейнер и свидетельства — Proof-Carrying .kimg (проверка вшитого
    доказательства без Z3, PATH может быть пустым), затухание устаревших
    свидетельств (T → N), Merkle-цепочка журнала вердиктов, Bit-Rot Guard.
  3. Автопилот без контрактов — --xray (мёртвые ветки, избыточные гарды,
    пути падения, границы, сложность Маккейба), --gen-tests, --infer-requires,
    [SUGGESTED FIX], --simplify, --explain, --pr-summary.
  4. Математика — циклы (invariant/decreases, 4 обязательства Флойда),
    границы массивов без аннотаций, IEEE-754 NaN и QF_S с trusted: 0,
    инварианты состояний.
  5. Массовость — 7 языков, однословные пресеты, анти-арбитраж (DeFi),
    двойное списание, FFI-границы, SQL/RLS, тарифные матрицы.
  6. Щит ИИ — анти-чит (__eq__, sys.exit, mock, оверфиттинг),
    --audit-mcp + замок схемы, @kern:secret (2-safety), рой Белнапа.
  7. Парадигмы — Action/FinOps Firewall, поиск противоречий в документах,
    RLVR-оракул вознаграждения, полевой bug_hunter.
  8. Упаковка — WASM, интерактивный --html, kernc grep по .kimg,
    8 MCP-инструментов, install.sh, tests/fuzz_corpus/, --audit-repo.

Дефекты, найденные этими же инструментами

Полный журнал — docs/CAPABILITY_STATUS.md (§6c–§6d) и docs/METRICS.md
(§70–§116): #123–#184. Три примера того, что «зелёный CI» не равен корректности:

  • #155 — пруф-чекер принимал подделку: переименование определения шага
    @x147 → @x9 давало farkas 3 → 0, trusted: 0, rc=0. Исправлено: битая
    ссылка @xN — отказ.
  • #166 — builtin_lia выбирал переменную с нулевым коэффициентом → ложный
    unknown в kernc.wasm там, где CLI отвечает SAT.
  • #173 — предохранитель свидетельств обвинял сам харнесс (в базисе
    лежали артефакты, которые прогон пересобирает; снимок перезаписывался посреди
    прогона). Теперь снимок write-once, продукты исключены, грязный старт → rc=3.

Как проверить релиз

# 1) скачать и сверить бинарник
curl -fsSLO https://github.com/newmathphys/kern/releases/download/v2.5.0/kernc-x86_64-linux-musl
curl -fsSLO https://github.com/newmathphys/kern/releases/download/v2.5.0/SHA256SUMS
sha256sum -c SHA256SUMS
./kernc-x86_64-linux-musl --version

# 2) проверить аттестат (Ed25519, без внешних сервисов)
python3 tools/slsa_provenance.py --check      # АТТЕСТАТ ВАЛИДЕН

# 3) убедиться, что гейты способны падать (это и есть смысл can-fail)
python3 tools/canfail.py --check-anchors

Честные ограничения

  • Экстрактор работает на подмножестве (линейная арифметика, if/else,
    машинные границы); всё остальное — SKIP с причиной, а не «доказано».
  • Для Python нет информации о типах: атрибут может моделироваться как Int.
  • Пруф-чекер консервативен: непокрытое правило даёт trusted > 0, и это
    никогда не выдаётся за trusted: 0.
  • align(32) в blake3_simd8 не дал измеримого ускорения (2.42 против
    2.41 GB/s) — оставлен как безвредная правка, без заявления о выигрыше.
  • tools/kern_contracts.py содержал 52 дублирующихся определения (дефект
    #174). ЗАКРЫТО: удалены все затенённые копии (52 → 0, −2003 строки),
    tools/dup_defs_guard.py зажат в базис 0; попутно найден второй
    if __name__ == "__main__" (вызывал main() до определения функций второй
    половины файла — отсюда прежний NameError: cmd_xray) и восстановлена
    маршрутизация _xray_clike_file (в РАННЕЙ копии cmd_xray она была новее,
    но исполнялась МЁРТВАЯ поздняя — C-like просто не сканировался);
    перестройка файла — отдельная работа.
  • Лицензия PolyForm Noncommercial 1.0.0 (source-available): коммерческое
    использование требует лицензии от правообладателя.
Assets 4
Loading