Verified Relay R1 — Direction State Validation

Отдельный эксперимент проверяет восемь чистых функций examples/apps/relay/direction.liza, используемых TCP-прокси. 16 обязательств: для каждой функции отсутствие trap и точное совпадение результата с независимой спецификацией, включая полноту покрытия путей. Восемь мутаций исходника обнаруживаются и воспроизводятся отдельным конкретным интерпретатором Semantic IR.

R1 проверяет координаты очереди. Он не доказывает сохранность байтов, корректность сетевого runtime, LLVM или машинного кода прокси. Проверки V0–V4, общий verification pipeline и направление Verification Bundle не меняются.

Контракт

Входы — все значения u32 для head, tail, count, включая 0xFFFFFFFF, и все комбинации eof/fin. Предположения о корректности входного Direction нет. Неверное состояние также должно обрабатываться без trap.

Спецификация независимо определяет:

Valid(d) = 0 <= head <= tail <= 2048
           and (fin implies (eof and head == tail))
ReadyFin(d) = Valid(d) and eof and head == tail and not fin

Функция	Ожидаемый результат
empty	(0, 0, false, false)
valid	В точности Valid(d)
readable	2048-tail, если Valid(d) и нет EOF; иначе 0
queued	tail-head, если Valid(d); иначе 0
read	Err, если состояние неверно, есть EOF, tail=2048 или count>2048-tail; иначе переход ниже
write	Err, если состояние неверно, count=0 или count>tail-head; иначе переход ниже
needs_fin	В точности ReadyFin(d)
shutdown	Ok(head,tail,true,true) при ReadyFin(d); иначе Err

Успешный read(0) устанавливает EOF, сохраняя координаты и снимая FIN. Положительный read увеличивает tail на count, оставляя head и устанавливая eof=false, fin=false. При полностью заполненном буфере read(0) возвращает Err: приложение сначала должно освободить место для следующего чтения.

Успешный write увеличивает head на count. Если очередь опустела, оба индекса сбрасываются в ноль; eof и fin сохраняются. Все ошибки — Err(Error.InvalidTransition). Сравнение включает тег Result и активный payload.

Что исполняет проверяющий инструмент

Исходник сохраняется побайтно без изменений. Маленький import-harness позволяет обычному компилятору получить Semantic IR модуля. Сериализованный JSON сохраняется и затем читается независимым интерпретатором. Значения вычисляются из операций, ветвлений, phi и тел вызываемых функций. may_trap и storage_contract не используются как аксиомы.

Поддерживается Semantic IR версии 20, чистый ациклический CFG, скалярные вызовы вспомогательных функций, u32, bool, структура Direction и её Result/Error. Инструкции: constant, struct.construct, struct.field, variant.construct, phi, call, not, eq, ule, ugt, checked add/sub; терминаторы return, branch, jump. phi выбирается по предшественнику. Циклы, рекурсия, эффекты и неподдерживаемые операции дают unknown.

Для u32 интерпретатор использует математические целые с диапазоном [0, 2^32-1]. Переполнение checked-операции создаёт отдельный исход Trap. Каждая ветвь имеет собственное условие достижимости, поэтому неисполняемая арифметика не вызывает trap. Например, readable при tail=0xFFFFFFFF возвращает 0, не вычисляя 2048-tail.

Два SMT-запроса на функцию ищут: достижимый Trap; либо Trap, неверный результат или непокрытый исход. unsat означает доказанное обязательство в этой модели. sat подтверждается отдельным конкретным исполнением того же IR на Python-значениях, без Z3 и без вызова символического интерпретатора. Если свидетельство не воспроизводится, результат — unknown, а не установленный дефект программы. Тайм-аут также даёт unknown и не позволяет эксперименту завершиться успешно.

Отрицательные контроли

Каждый контроль меняет именно Liza-исходник, заново компилируется и сохраняет свой IR. Спецификация остаётся неизменной.

Мутация	Нарушение
Удалена проверка tail<=2048	Принято недопустимое состояние
Вместимость 2047-tail	Неверный результат или Trap
queued возвращает tail	Не учтён уже отправленный префикс
Удалён предел count в read	Неверный переход или переполнение
read(0) не устанавливает EOF	Потеря EOF
write не продвигает head	Потеря прогресса
write не обнуляет пустую очередь	Неверное конечное состояние
shutdown допускает непустую очередь	Преждевременный FIN

Например, удалённая проверка count допускает tail=1, count=4294967295: конкретное исполнение подтверждает trap на сложении. Значения остальных свидетелей выбирает решатель; фиксированный конкретный вход не является доказательством для всех входов.

Воспроизведение и артефакты

Из корня репозитория, в окружении с зависимостями verification/requirements.txt:

python -m unittest verification.relay_r1.test_model -v
python -m verification.relay_r1.check --output build/verified-relay-r1

Каталог вывода должен быть новым или пустым, чтобы не смешивать артефакты разных запусков. По умолчанию на каждый SMT-запрос отводится 10000 мс; положительный лимит можно изменить через --timeout.

Сохраняются оригинальный исходник, harness, восемь мутантов, фактический IR, SMT-LIB запросы, результаты и конкретные трассы. tools/ содержит копии Python-исходников компилятора и проверяющего инструмента, независимую спецификацию и закреплённые зависимости. Отчёт фиксирует версии Python/Z3/IR, лимит решателя, область проверки и SHA-256 артефактов. Сам отчёт не включён в собственный список хешей; он не подписан и не является сертификатом доказательства или герметичным bundle.

Отдельный workflow запускает тесты и полный R1 на Linux, macOS и Windows и публикует артефакты. Успешный статус требует всех 16 доказанных обязательств и всех восьми подтверждённых мутаций. Обычной сборке Liza решатель не нужен.

Доверенная база и следующий шаг

Доверенная база включает спецификацию, интерпретатор IR, сериализацию IR, Python и Z3. Это проверка конкретных функций конкретного сохранённого IR, не универсальная теорема о компиляторе или любой пользовательской программе.

Ранее созданная математическая модель verification/relay_model продолжает отдельно проверять R = W ++ Q. R1 не связывает её последовательности с реальными чтениями и записями регионального буфера.

Будущий R2 — Byte Conservation должен проверить связь R = W ++ Buffer[head:tail] с фактическими операциями программы. До этого проверенные координаты не означают доказанную сохранность передаваемых байтов.