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

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): коммерческое
  использование требует лицензии от правообладателя.

KERN v2.4.0 — Hardcore Audit & C-ABI Hardening

KERN v2.4.0 completes the industrial hardcore audit: five destructive
checks aimed at the failure modes that normal tests never reach, plus the
human-facing features that make the tool usable without writing SMT-LIB by hand.

Security & robustness (found REAL defects)

• Deep Nesting Bomb (#98). parseList recursed without a depth limit. Measured:
  '(' * 50 000 survived, '(' * 2 000 000 → terminated with signal SEGV.
  Solver output is untrusted input, so this was a denial of service from a single
  .smt2 file. Fixed with ParseError.TooDeep + MAX_SEXP_DEPTH = 4096.
• NULL pointers in the C-ABI (#99). C callers can pass NULL where Zig's
  [*]const u8 cannot represent it; img[0] on NULL crashed the caller's
  process. Fixed with isNull() (@intFromPtr) in all 8 exported functions.
  Verified by tests/c_abi_test.c built with
  zig cc -Wall -Wextra -Werror -pedantic -std=c11 — 20/20.
• Header type mismatch (#100). Strict flags rejected passing
  unsigned char[64] to kern_localize, which was declared char *out_buf
  while every other function used unsigned char *. Header aligned.
• Memory leak under partial OOM (#101). try out.append(try allocator.dupe(...))
  in extractAsserts leaked the duplicate when append failed. Found by
  std.testing.checkAllAllocationFailures (fails at every allocation).
  Fixed with errdefer.

Concurrency

• 8-thread stress through the real shared library. In test builds Zig's
  builtin.is_test short-circuits compat.io() to std.testing.io, so the
  threadlocal var tls_io cache is never exercised by zig build test.
  A C test (tests/c_abi_threads.c) now drives it through libkern.so:
  8 threads × 500 kern_hash → 0 divergences; 8 threads × 20
  kern_smt_verify → 0 errors, 160/160 proved. The reference digest is a
  constant (cross-checked against an independent BLAKE3), otherwise a
  mutation inside the hash path would change both sides of the comparison.

Tooling honesty

• Mutator covered only the old core (#102). TARGETS was a hard-coded list
  of 6 files, so every module added in v2.2–v2.4 was never mutated and the
  previously reported score said nothing about them. Now 14 files / 427 sites
  (was 6 / 63).
• C-ABI was outside mutation coverage (#103). zig build test never runs the
  C tests, so mutations in src/capi.zig survived. The mutator now rebuilds
  libkern.so from mutated sources and runs both C tests.
• Attestation fixes (#87, #92). The SLSA attestation no longer hashes its own
  evidence logs (circular), and it now attests the reproducible release artifact
  kernc-hermetic instead of Debug binaries that any zig build overwrites.

Human-facing features

• # @kern:ensures now accepts if/elif/else and local assignments (translated
  to SMT ite); out-of-subset code is reported as SKIP with a reason.
• Z3 counterexamples are printed in the CLI: [КОНТРПРИМЕР] balance = 0, amount = -1, result = 1.
• kernc build --deflate — object compression (measured 3.16× smaller image).
• examples/kern_mcp_server.py — MCP server with 4 tools for Claude Code / Cursor.

Verification baseline

Check	Result
Core tests (Debug + ReleaseSafe)	251 / 251
KERN-Next (kernx)	37 / 37
Lean 4 proofs	7 files, 0 errors, 0 sorry
canfail non-vacuous checks	72 / 72 CHECK targets with a proven-can-fail case (85 cases)
Mutation score (Zig-native mutator)	77.5 % (31 / 40 killed) over 14 files / 427 sites (was 6 / 63 before this release)
Defect registry	#1–#103, numbers unique
Evidence gate	all logs RC=0
SLSA attestation	VALID (unsigned — no cosign; recorded in kern:notes)

KERN v2.2.0 - Independent Z3 Proof Checker (Farkas/Resolution) & 8-Way SIMD BLAKE3 (3.42x)

KERN v2.2.0 introduces two major engine upgrades: an independent mathematical verifier for native Z3 proof DAGs and an 8-lane SIMD multi-buffer BLAKE3 engine for small-object verification.

1. Independent Z3 Proof DAG Checker (src/verifier/proof_check.zig)

Instead of trusting solver unsat output as an opaque string, KERN parses and mathematically audits native Z3 S-expression proof DAGs across 6 invariants:

• No proof holes: immediate rejection on hole, trust, or sorry steps.
• Premise binding: every nested (asserted ...) node is recursively matched against the normalized clauses of the input contract (premises_unbound == 0).
• Modus Ponens structure: verifies implication/equivalence matching between premises.
• Unit resolution: verifies that every resolved literal is refuted by its premise literals.
• Farkas' Lemma arithmetic: normalizes linear integer inequalities (negation of l <= r is r - l + 1 <= 0 over Z), applies Farkas weights, and verifies that all variable coefficients cancel to 0 while yielding a strictly contradictory positive constant.
• Root contradiction: the DAG must conclude false.

Scope note: internal Z3 rewrite steps are tracked separately in trusted_steps and are not claimed as independently re-derived. Alethe is not used: this Z3 build does not emit it (strings z3 | grep -ic alethe -> 0; no proof.format option). See docs/METRICS.md section 48.

2. 8-Way SIMD BLAKE3 Batch Engine (src/core/blake3_simd8.zig)

Single-chunk objects (<= 1024 B) cannot saturate 8-lane AVX2 chunk parallelism when hashed one by one. The engine hashes 8 objects of arbitrary individual lengths simultaneously across @Vector(8, u32) lanes using per-lane @select masking, without altering a single byte of the .kimg format. Each of the 8 results is still compared against its own 32-byte entry.digest.

Workload (10,000 objects, Intel i7-7700 AVX2)	Scalar	8-Way SIMD	Speedup
Isolated primitive - 96 B	352 MB/s	1,939 MB/s	5.51x
Isolated primitive - 200 B	369 MB/s	1,834 MB/s	4.97x
Isolated primitive - 512 B	537 MB/s	2,395 MB/s	4.46x
Isolated primitive - 1024 B	550 MB/s	2,728 MB/s	4.96x
End-to-end .kimg safe read (200 B)	356 MB/s	1,219 MB/s	3.42x
Single-read loop via cluster cache	387 MB/s	1,699 MB/s	4.39x

Raw unverified zero-copy slice addressing runs at ~102 GB/s; the end-to-end gap drops from 287x to 84x.

3. Cluster Cache for Per-Object Reads (KernFS.objectPayloadCached)

A 1-bit-per-object bitset (1250 bytes for 10,000 objects): the first access to any object verifies the whole cluster of 8 neighbours in one vector pass, and bits are set only after all eight match their own digests. Precondition, stated plainly: the cache is valid only for an immutable image (mmap of a sealed file); for mutable buffers objectPayload / verifyAllBatch / payloadSlice remain the honest paths.

Verification Baseline

• Core tests: 220 / 220 passed (+12 proof checker, +3 SIMD-8, +2 cluster cache, +1 linear rewrite verification, +2 boolean rules).
• Proof checker visible in the CLI: kernc prove formal/example.smt2 prints
  [PROOF VERIFIED] steps: 16 | premises bound: 1/1 | mp: 2 | rewrite (linear): 5 | farkas: 0 | trusted: 0 | holes: 0 - all 16 steps of that DAG are re-checked
  independently, with trusted_steps down to 0 (comparisons, linear arithmetic, mp, unit-resolution, Farkas, refl/symm/trans, and-elim, monotonicity).
• Static binary in Assets: kernc-x86_64-linux-musl (5,689,232 bytes, sha256 7f29d979...) - no toolchain needed, verify with SHA256SUMS.
• Non-vacuous canfail checks: 71 fault-injection cases registered; tools/registry.py reports 64/64 build targets covered with a proven-can-fail check (added proof-hole, proof-binding, simd8-masking).
• Evidence gate: all verification logs clean (RC=0).