herness

Харнесс — не один репозиторий, а сеть атомарных безопасных ячеек. Ячейка — это изолированная комната с объявленными границами; отношения между ячейками формально доказаны, поэтому части взаимозаменяемы: ядро можно вынуть и заменить, сохранив остальное. Мост между двумя ячейками не соединяется, если их пулы законов несовместимы — не «проверка при соединении», а невозможность соединения.

Подробно — docs/VISION-0001-harness-as-cell.md.

Идея

Инструмент — не функция, а договор между агентом и харнессом. Договор отвечает на три вопроса:

• что разрешено — политика;
• кто принимает решение — посредник;
• что доказано, а что только измерено — замыкание.

Из этого выводится всё остальное. Отсюда три уровня, и их нельзя смешивать:

уровень	что	доказуемо	где
A. Политика	кто, какое действие, над каким ресурсом	да, проверкой	lab/tools/policy.json
B. Посредник	код, который исполняет политику	да, для малого кода	core-rs/src/loopmod.rs
C. Замыкание	что ничто не пройдёт мимо посредника	нет, только измеряется	lab/tools/registry.jsonl

Правило: A и B — доказательство. C — измерение. Утверждать больше, чем доказано, здесь нельзя.

Что уже работает

слой	что это
ядро	свой Linux 6.18.60, tinyconfig, без модулей; namespaces, cgroups, Landlock, seccomp; стены — 25 из 29 (kernel_audit.py)
комната	QEMU + init/PID1 на Rust; нет shell и coreutils; инструменты не выходят из каталога
изоляция записи	openat2 + RESOLVE_BENEATH/RESOLVE_NO_SYMLINKS — симлинк наружу не проходит (F-0083)
изоляция сети	SSRF-фильтр исходящих URL (net_policy.py), netprobe проверяет адрес; restrict=on через guestfwd — честный отказ на Windows (F-0084)
цикл	модель отвечает одной строкой: TOOL <имя> <аргумент>, DONE <итог>, BLOCKED <почему>
политика	19 правил для шести инструментов; проверяется на четыре класса дефектов
посредник	решение о доступе принимает политика, а не код; её спрашивает каждый инструмент
журнал	HSJ2, append-only; CRC покрывает kind — подмена Data↔Commit детектируется; оборванный хвост карантинится (ADR-0056, F-0086)
приёмка	read-only с копии образа, SHA-256 до == после; критерий объявлен до прогона; живая приёмка комнаты HSJ2 — PASS (F-0085, F-0087)
гейты	32 гейта, два контура (механизм / целостность); у каждого проба на подложенный дефект — 32 из 32 (33 пробы)

Инструменты и их замыкания

инструмент	что делает	замыкание
search	ищет подстроку в файлах каталога	чтение /mnt, 2 с, 32 МБ
list	перечисляет содержимое каталога	чтение /mnt, 200 мс, 8 МБ
read	читает файл с номерами строк	чтение /mnt, 100 мс, 4 МБ
write	пишет файл внутри рабочего каталога	запись /mnt/work, 200 мс
seal	отпечаток содержимого до маркера	чтение /mnt, запись /mnt/work
netprobe	проверяет доступность адреса	только мост провайдера

Как проверяется

Каждая проверка — со своим отрицательным контролем (подложенный дефект обязан быть пойман):

проверка	что ловит	результат
policy.py --check	противоречие, неявное разрешение, цикл делегирования, правило без уровня	4 из 4
policy_sync.py	политика в коде разошлась с политикой в файле	совпадают (policy-sync.txt)
closure_probe.py	код выходит за объявленное замыкание	0 нарушений
registry_probe.py	реестр без хеша среды, без примеров, повтор версии	6 из 6
gate_probe.py	гейт не замечает подложенный дефект	33 из 33
policy_diff.py	две реализации одной функции расходятся	15 из 18 (3 — ограничение модели)
lean_check.py	доказательство не собирается или опирается на аксиому	6 теорем, 0 нестандартных
bridge_lean.py	мост нарушает адрес, токен или тело ответа	6 теорем, 0 аксиом
refusal_codes_probe.py	код отказа не из словаря	4 из 4
claims_audit.py	ожидание утверждения нельзя проверить	109 слабых из 295

Где мы сейчас

Числа пересобираются командой python bin/readme_numbers.py --fix из артефактов проверок.

показатель	значение
утверждений	301
ядро	17
покрытие	1.0
строгое покрытие	0.58
гейтов	32
проб гейтов	33 из 33
журналов в индексе	135
отказов	83
решений	45
pass@1	0.72
pass^2	0.50
ложных «готово»	0.03
цена принятого	0.0052
серия 50 задач	49 из 50

Что дало сдвиг — каждое с замером, а не с верой:

что	было	стало
петля по информации (тот же вызов + тот же результат)	84 % прогонов без исхода	застой останавливает прогон с причиной
правило «сколько разных — бери из N»	задача не решалась, 19 шагов	решена за 3 шага
правило «собери ответ из нескольких результатов»	цепочка не решалась	решена за 6 шагов из 20
поиск	регистрозависимый, окно 160 символов	регистронезависимый, окно сдвигается к совпадению
пробы гейтов	2 из 28	33 из 33

Чего это не доказывает

• Не работающий продукт. Нет релиза и нет выполненного внешнего задания.
• Не «умнее». Разница не в правильности ответов, а в том, что остаётся, чем проверить.
• Не полная изоляция. Нет shell, инструменты не выходят из каталога, Landlock включён, но это не защита от целевого обхода.
• Не «задача решена». Приёмка проверяет объявленные условия; если критерий неполон, PASS этого не покажет.
• Уровень C не доказан. Замыкание измеряется пробами, а не доказывается формально.
• Ядро не верифицировано. Стены закрыты (25 из 29 в конфиге, ещё 3 работают без опции, 1 не нужна), но код ядра не доказан — ошибка в нём остаётся возможной.
• Проба ловит известный дефект, не неизвестный. У каждого из 32 гейтов теперь есть отрицательный контроль (33 пробы, 32 из 32 гейта), но это проверка реакции на подложенный дефект, а не доказательство надёжности. Сам аудит считал покрытие неверно (F-0088: обрезал составные имена проб, считал строки вместо разных гейтов — 31/32 вместо честных 30/32) — прибору понадобился свой прибор (check_probe_coverage.py), и он ловит регрессию этого счёта, а не произвольную ошибку измерения.
• Покрытие 1.00 — это «якорено», не «строго проверяемо». Все 300 утверждений имеют команду, артефакт и ожидание (anchored 1.00), но строго проверяемых — 0.58 (172 из 297 активных): 109 ожиданий — общие слова («ок», «итог: PASS», «ПРИБОР ЧЕСТЕН»), 23 артефакта — описания без файла. Прибор покрытия льстил себе (F-0089: выдавал CHECKED_ANCHORED при anchored 1.00, скрывая strict 0.58) — теперь он показывает обе меры рядом и понижает вердикт до ANCHORED_WEAK, а свой прибор (check_coverage_verdict.py) ловит регрессию этой честности (красный до / зелёный после). Strict меряет форму ожидания (число/путь/код), не истинность: 0.58 ≠ «42% утверждений ложны». Anchored-порог и инвариант аудита не ослаблены — ANCHORED_WEAK добавлен как понижение.

Границы — NOT-CLAIMED.md, отброшенное — docs/eliminations.md, отказы — lab/failures/.

Структура репозитория

core-rs/          ядро, init/PID1, цикл, посредник; сборка и прогоны в QEMU
  src/loopmod.rs  цикл и ПОСРЕДНИК: политика, проверка доступа, инструменты
  src/journal.rs  журнал HSJ2: CRC покрывает kind, карантин оборванного хвоста
  kernel/         конфиги ядра: minimal, hardened, hardened2, net, rng
  build.ps1       musl-сборка hs-core; accept-run.ps1 / crash-resume.ps1 — прогоны
bin/              гейты и проверки (хост)
  hs.py           все гейты одной командой (два контура)
  policy.py       политика: сборка и четыре проверки
  policy_sync.py  политика в коде против политики в файле
  closure_probe.py код против объявленного замыкания
  net_policy.py   SSRF-фильтр исходящих URL
  kernel_audit.py аудит стен ядра
  gate_probe.py   пробы гейтов (подложенный дефект)
  audit.py        повторяемый аудит репозитория
  readme_numbers.py числа README из артефактов
  build_room.py   сборка образа комнаты по манифесту
  extract_journal.py read-only извлечение журнала с копии
  bridge.py       хост-мост к модели
lab/              отказы, склад решений, пре-регистрации, манифест комнаты
  tools/          policy.json, registry.jsonl, contracts.json
  prereg/         пре-регистрации с порогом ДО прогона
  registry.json   реестр опытов и гипотез
  failures/       находки F-XXXX: отрицательный результат остаётся
proofs/           Lean-доказательства политики и моста
accept/           критерии приёмки — в комнату не попадают
docs/             ADR, видение, план аудита, карта сессии, журнал решений
research/         склады источников, артефакты прогонов, задания на ресёрч
parts/            части харнесса: независимые ячейки (flowguard-spec, lexspec, VecDHT, nomos)
CLAIMS.md         реестр утверждений: тип свидетельства, команда проверки, граница

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

python bin/hs.py gates            # 32 гейта (два контура) + пробы
python bin/audit.py               # повторяемый аудит: числа, долги, инварианты
python bin/policy.py --check      # политика: четыре проверки
python bin/policy_sync.py         # политика в коде против файла
python bin/closure_probe.py       # код против замыкания
python bin/kernel_audit.py        # стены ядра
python bin/gate_probe.py          # полный набор проб гейтов
python bin/judge_metrics.py       # pass@1, pass^2, ложное «готово»
python bin/readme_numbers.py --fix # пересобрать блок чисел README из артефактов
python bin/lean_check.py          # формальная проверка политики в Lean
python bin/bridge_lean.py --check # формальная проверка моста
python bin/policy_diff.py         # сверка Rust и Lean
python bin/refusal_codes.py --list # коды отказа

Прогон в своём ядре (закалённом, hardened2) и живая приёмка комнаты:

python bin/bridge.py              # хост-мост к модели (deepseek-v4.1-flash)
python bin/build_room.py --build  # собрать образ комнаты по манифесту
pwsh core-rs/run.ps1
pwsh core-rs/accept-run.ps1 -Mode loop-bridge -Kernel vmlinuz-own-hardened2 -Net -Criteria accept/room-smoke.json
pwsh core-rs/crash-resume.ps1 -KillAfterSec 30

Токен моста скрипты читают в рантайме из файла вне репозитория; значение не попадает в контекст и в git. guestfwd/restrict=on на Windows канал не поднимает (F-0084) — изоляция сети обеспечивается SSRF-фильтром и проверкой адреса, а не restrict=on.

Куда движемся

Порядок выведен из того, что доказуемо, а не из интереса.

Сделано:

1. Посредник для всех шести инструментов — политику спрашивает каждый.
2. Стены ядра — 25 из 29 в конфиге, ещё 3 работают без опции, 1 не нужна; недостающих нет.
3. Формальная верификация политики и моста — 6 + 6 теорем в Lean, только стандартные аксиомы.
4. Коды отказа — 19 кодов, серия размечена.
5. Изоляция и целостность ядра (аудит, этапы 1.1–1.6 и 2.1): SSRF-фильтр, запись через openat2, read-only приёмка с копии, журнал HSJ2 (kind внутри CRC), живая приёмка комнаты — PASS. Карта этапов и статусы — docs/AUDIT-PLAN.md.

Дальше:

1. CI-гейт версии бинарника — ловить дрейф «исходник новее бинарника» (урок F-0087); робастность crash-resume к раннему крашу (F-0027).
2. Отношения между частями — что значит «часть», «отношение», «взаимозаменяема»; тогда части можно менять, включая ядро (docs/VISION-0001-harness-as-cell.md).
3. Замыкание как измерение — пробы выхода для каждого инструмента.
4. Три режима работы — план, автономное выполнение, долгосрочная цель.

Подробно о переходе — docs/TRANSITION-0001-policy-mediator-closure.md; где остановились — docs/WHERE-I-STOPPED.md.

Честная оценка по чужой рубрике

Приложим к себе рубрику proof-of-usefulness (HackerNoon), потому что она взвешена по причинам провала стартапов, а не по удобству автора:

критерий	вес	у нас
реальная польза	25 %	частично: механизм работает, но ни один человек не изменил решение
свидетельство использования	25 %	0: ноль пользователей
охват и влияние	20 %	0: нет публикации, нет аудитории
новизна и устойчивость	15 %	сильная: две реализации (Rust и Lean), пробы гейтов, формальные доказательства
своевременность	10 %	спорно
полнота	5 %	да

50 % — польза и использование. По этой арифметике мы — 15–20 из 100. Движок готов, свидетельства использования нет. Это и есть настоящий разрыв.

Потолок дизайна

Всё, что инструмент «пересчитывает», пересчитывается из того, что написал агент. Честный потолок не «агент не соврёт», а «документ лживого агента противоречит себе» — и это видно при чтении, а не доказывается автоматически.

Аудит гейтов (bin/gate_audit.py) находил слабые места там, где автор сам выбирает, чем подтвердить (опора и утверждения). Эту форму дефекта flowguard-spec ловил десятки раз за несколько раундов — она не исчезает от добавления гейтов, её закрывают контрактом на стыке.

Три правила этого репозитория

1. Число без команды — не результат. У каждой цифры рядом команда и артефакт.
2. Отрицательный результат остаётся. docs/eliminations.md, lab/failures/, отклонённые решения в складе — не свалка.
3. Каждый отчёт содержит раздел «что это не доказывает».

Подробнее — AGENTS.md. Реестр утверждений — CLAIMS.md. Границы — NOT-CLAIMED.md.