Liza Verified Network Gateway

Цель следующего этапа, а не название уже верифицированного продукта. Конфигурируемый L4 TCP-прокси с ограниченными ресурсами, корректным half-close, управляемым завершением, измеренной производительностью и воспроизводимыми свидетельствами проверенных свойств.

Liza — системный язык для производительных сетевых сервисов с определённым поведением, контролируемыми ресурсами и математически проверяемыми свойствами. Производительность и область доказательства подтверждаются отдельно для конкретного приложения, исходников и инструментария.

База и ближайшая работа

В main уже есть examples/apps/liza_proxy_ops.liza: первый срез 0.0.31 реализует net.Address, CLI listener/upstream, монотонное время и connect deadline. Их не нужно проектировать заново. Сейчас — восемь пар, один поток ОС и 32 КиБ пользовательских relay-буферов; память runtime и ОС учитывается отдельно.

Эксплуатационный срез расширяет этот пример: idle timeout, graceful shutdown с конечным drain, метрики и тесты освобождения ресурсов. Реализованный CLI и команды воспроизведения описаны в документации proxy operations. Исходный liza_proxy.liza 0.0.30 остаётся регрессионной базой Relay. Новые возможности stdlib/runtime добавляются только под эти контракты.

Далее зафиксирован контракт приёмки. Реализация lifecycle не закрывает отдельные задачи baseline, Verified Networking и независимой приёмки релиза.

Idle timeout

Для установленной пары сохраняется время последнего успешного переноса n > 0 через read или write любого направления. Отсчёт начинается при принятом завершении connect. Ожидание connect сохраняет собственный deadline.
Readiness, WouldBlock, Interrupted и повторный poll не продлевают idle. EOF/FIN сами по себе не являются передачей данных и не сбрасывают этот таймер.
Используется elapsed-time: сначала проверяется now >= started, затем now - started >= timeout. Регресс часов/ошибка часов обрабатывается явно; wrapping, отрицательный интервал и бессрочное продление не допускаются. Ненадёжные часы завершают сервер с ошибкой и закрытием ресурсов; продолжение timed drain без достоверного времени не обещается.
Истёкший idle закрывает всю пару, включая оба направления и очереди. Это эксплуатационная политика, а не нормальный EOF и не обещание доставки. Медленный получатель тоже может привести к idle timeout, если переносов нет.
Время poll ограничено ближайшим оставшимся сроком. Перед новым I/O проверяются уже истёкшие сроки; активность другого клиента не продлевает эту пару.

Graceful shutdown и half-close

Предлагаемый жизненный цикл сервера: Running → Draining → Stopped.

После того как event loop наблюдал запрос остановки:

Новые accept не выполняются. Уже принятые пары остаются активны.
Listener исключается из readiness и закрывается/деактивируется без закрытия клиентских сокетов. Простого if !stopping вокруг accept недостаточно: нынешний reactor включает listener в poll при наличии свободного слота, и ожидающие подключения способны вызвать busy-loop во время drain.
Для существующих пар продолжаются оба направления I/O, backpressure и проверка connect/idle deadlines. Запрос остановки сам по себе не является EOF.
FIN передаётся только после EOF источника и полного опустошения очереди соответствующего направления. Второе направление продолжает работать.
При естественном завершении всех пар сервер закрывает reactor. Иначе фиксированный срок drain принудительно завершает оставшиеся пары.

Срок drain не перезапускается от новых байтов, readiness или повторного запроса остановки. Непрерывно пишущий клиент не может продлить его бесконечно. Pending connect ограничен минимумом своего исходного срока и оставшегося drain.

При истечении drain досылка не гарантируется: неотправленные пользовательские очереди отбрасываются, оба ID инвалидируются. Принятые локальным сетевым стеком байты также не являются подтверждением доставки удалённому приложению. RST и другие фатальные ошибки сохраняют политику завершения всей пары.

При одновременном истечении сроков нужна одна фиксированная причина завершения: сначала общий drain, затем connect или idle соответствующей фазы. Пара учитывается в счётчиках закрытия один раз. Время ожидания ограничивается в работающем event loop; жёсткая realtime-гарантия при задержках ОС/планировщика не заявляется. Вывод метрик не должен удерживать сокеты после срока остановки.

Системное уведомление должно передавать запрос в event loop с ограниченной задержкой; ресурсные операции, аллокации и сложная логика не выполняются в асинхронном обработчике. Поддержанные способы остановки документируются отдельно для POSIX и Windows, без обещания одинаковых механизмов ОС.

Метрики и лимиты

Метрика	Семантика
active pairs / accepted / closed	Текущее число пар и счётчики их жизненного цикла
bytes read / bytes written по направлениям	Успешные count; write означает приём локальным стеком
errors	Терминальные ошибки, отдельно от ожидаемых WouldBlock/Interrupted
connect / idle timeouts	Завершения по соответствующему deadline
drain forced closes	Пары, принудительно закрытые по общему сроку
discarded user-queue bytes	Байты в пользовательских очередях при сбросе, не оценка всей сетевой потери

Первый срез сохраняет восемь пар и фиксированные буферы. Метрики не создают очередь неограниченного размера или обязательную запись на каждый байт. Для накопительных u64-счётчиков нужно определить насыщение с признаком overflow: телеметрия не должна приводить к обязательному arithmetic trap долгоживущего сервера или молча оборачиваться. Gauge активных пар остаётся точным.

Приёмка использует управляемые часы и запрос остановки, реальные loopback-сокеты и O0/O2 на Linux/macOS/Windows. Обязательны: границы каждого deadline, неактивная пара рядом с работающей, slow reader с полной очередью, half-close с ожидающим ответом, shutdown во время connect, reset, повторная остановка, непрерывный вход до drain deadline и повторное использование освобождённых ID.

P0 — Verified Networking

R1, R2-A, R2-B и R2-C имеют разные области проверки. R2-C замыкает выбранный фрагмент одной пары baseline 0.0.30 при контрактах runtime; он не доказывает runtime, произвольное взаимодействие всех пар или новый CFG liza_proxy_ops.

Следующая исследовательская работа — контрактная модель сетевой границы, независимые проверки адаптеров и контролируемый fault injection:

read/write: точный диапазон памяти, короткие успешные переносы и границы 0 <= n <= requested; успешный write непустого диапазона обязан вернуть n > 0;
EOF при ненулевом запросе чтения и отдельный контракт нулевой длины;
WouldBlock без скрытого успешного переноса; readiness не является разрешением, гарантирующим успех следующего I/O;
shutdown_write, завершение connect и сохранение терминальной ошибки;
owner/generation/slot, чужие и устаревшие ID, повторное использование системного дескриптора, исчерпание поколений и полное освобождение пары;
допустимые побочные эффекты при Err, без автоматической аксиомы «ошибка ничего не изменила».

Fault-injection сценарий должен задавать согласованную последовательность вызовов, результатов, байтов и ошибок, а не независимый произвольный результат каждого шага. Сохраняются трасса, версия адаптера, исходники, seed и replay. Модель проверяется отдельно от реализации; реальные socket-тесты дополняют её.

Это не полная верификация POSIX/Winsock или ОС. Перенос Relay-гарантий на операционный proxy, затем validation lowering сетевых операций и машинного исполнения — отдельные доказательные шаги. Новые хеши и CFG требуют новой проверки. Успешные тесты не устанавливают end_to_end_verified=true.

Verification Bundle остаётся отдельной работой по переносимости свидетельств: целостность и воспроизведение не расширяют математическое покрытие.

P1 — измерения до масштабирования и MT

Сначала нужен воспроизводимый baseline восьми пар: throughput, распределение latency, CPU, RSS, стоимость poll/обхода таблицы, число системных вызовов, медленные клиенты, duplex и разные размеры передач. Фиксируются исходники, O0/O2, ОС, CPU, параметры нагрузки, расположение генератора и upstream, сырые серии и условия завершения. Инструментированные и обычные прогоны различаются; стоимость сбора измерений учитывается отдельно.

После управляемого освобождения и baseline — эксперимент с 1024 парами, не обещание текущей вместимости. При двух участках по 2048 байта это 4 МиБ пользовательских буферов; сокеты, runtime, таблицы и память ОС сверх этого. Текущий runtime ограничен 32 слотами и потребует отдельной работы для такого опыта.

Необходимость масштабируемого backend определяется измерениями. Кандидаты — epoll для Linux, kqueue для macOS; модель Windows выбирается отдельно. Одинаковая стоимость на трёх ОС не обещается.

MT начинается после измерения однопоточного сервера: изолированные workers, передача владения и bounded channels с backpressure. Сначала фиксируются допустимые передаваемые типы, региональные зависимости и завершение workers. M0 задаёт локальную исключительность, но не публикацию данных и синхронизацию. Shared mutable state, mutex и atomics — последующие самостоятельные этапы.

P2 — прикладные библиотеки

T4 нужен для конфигурации, JSON API и управляющих протоколов сетевых сервисов. После tokenizer расширение текстовой подсистемы приостанавливается, если нет конкретного сетевого потребителя. Универсальная stdlib не является самостоятельной целью. Self-hosting и frontend компилятора на Liza отложены без планового срока; Python-компилятор продолжает развиваться как основной инструмент.

Критерий готовности gateway — эксплуатационные тесты, опубликованные измерения на конкретном стенде и воспроизводимые свидетельства с точными границами покрытия. Название Verified не заменяет этих результатов.

Приёмка первого публичного релиза: независимое воспроизведение

Релиз принимается только после воспроизведения сторонним инженером из чистой рабочей копии конкретного commit, без файлов исходного рабочего окружения. Количество функций, тестов и доказательных обязательств не заменяет эту проверку. Набор воспроизведения должен содержать:

точный commit, версии и хеши инструментария, команды установки и сборки;
команды запуска upstream, proxy, генератора нагрузки и эксплуатационных тестов, включая управляемые часы, остановку и fault injection;
параметры стенда и нагрузок, сырые измерения и команды получения отчёта;
перечень проверенных свойств с привязкой к исходнику/IR и отдельный перечень предположений о runtime, ОС и lowering;
ожидаемые результаты корректности, платформенные ограничения и явные unknown для неподдерживаемых проверок.

Численные результаты производительности относятся к указанному стенду: воспроизводимость процедуры не обещает одинаковый throughput на другой машине. Первый публичный релиз требует опубликованного результата независимого прогона; до него gateway остаётся разрабатываемым рубежом, даже при зелёном CI.