Bounded L4 TCP Proxy · 0.0.30
Реализованный прикладной этап. Proxy передаёт произвольные бинарные TCP-потоки между клиентами и одним фиксированным upstream. До восьми пар, один поток ОС, IPv4 loopback. HTTP, TLS, балансировки и маршрутизации по данным нет. Message Router и echo-reactor сохранены самостоятельными примерами.
По умолчанию listener — 127.0.0.1:9004, upstream — 127.0.0.1:9003.
Upstream задаётся один раз в main (var upstream:u16=9003); для изменения
порта нужно изменить эту настройку и пересобрать приложение. Это прозрачный
relay: например, Message Router на 9003 сохраняет свой протокол за proxy.
--ephemeral выбирает порт listener через ОС, не меняя upstream. --once
также выбирает порт listener через ОС, обслуживает одну пару и выходит.
Выбранный порт выводится в stdout с LF. Коды выхода: 0 — нормальное завершение
обоих направлений, 2 — неверные аргументы, 3 — ошибка I/O/создания/закрытия.
В постоянном режиме ошибка отдельной пары закрывает только её два сокета.
Расширение reactor
Существующие Core, Semantic IR и правила владения не меняются. Добавлены
операции stdlib, их приватные ABI-адаптеры и реализация в socket runtime.
Все три операции имеют эффект io и заимствуют reactor.
| Операция | Результат |
|---|---|
net.reactor_connect(reactor, port:u16) |
Result<net.Connection,ReactorError>; новый исходящий IPv4 loopback-сокет принадлежит reactor, даже пока подключается |
net.reactor_finish_connect(reactor, id) |
Result<bool,ReactorError>; Ok(false) — Connecting, Ok(true) — Connected, Err — ошибка проверки или подключения |
net.reactor_shutdown_write(reactor, id) |
Result<u32,ReactorError>; закрывает только направление записи, сохраняя чтение и владение |
Порт upstream 0 даёт InvalidRange. Full не создаёт сокет. При немедленной ошибке connect временный сокет закрывается до возврата Err. Успешный возврат ID не означает Connected: после него вызывается finish_connect.
Исходящий сокет неблокирующий до connect. Его начальный интерес — запись.
На POSIX EINPROGRESS/EALREADY/EINTR означают продолжающуюся попытку; на Windows
учитываются соответствующие Winsock pending-коды. Завершение проверяется свежим
опросом с нулевым тайм-аутом, затем getsockopt(SOL_SOCKET, SO_ERROR).
Ноль в SO_ERROR без признака завершения не объявляется успешным connect.
На Windows проверка завершения использует write/exception sets select;
основной reactor по-прежнему использует WSAPoll.
См. контракт POSIX connect и контракт Winsock select. Готовность к записи — повод проверить состояние, а не доказательство успеха.
Ненулевой SO_ERROR сохраняется как терминальная ошибка слота. Последующие finish_connect не перечитывают очищаемый SO_ERROR и не превращают отказ в успех. Неизвестные ошибки, включая connection refused в текущем отображении, — Other. Ошибки самого опроса могут быть Interrupted; приложение сохраняет состояние и повторяет проверку. Терминальная ошибка connect не возвращается как временный WouldBlock/Interrupted. После ошибки ID остаётся собственностью reactor до disconnect/close.
Пока слот Connecting, read/write/shutdown_write возвращают WouldBlock без передачи данных. После терминальной ошибки они возвращают сохранённую ошибку. Для принятых через accept сокетов состояние сразу Connected.
Успешный shutdown_write запоминается: повторный вызов успешен без повторного системного shutdown. Write после него возвращает Disconnected, read остаётся разрешённым. Ни shutdown_write, ни ошибка connect не освобождают слот сами по себе. Чужие и устаревшие ID по-прежнему дают InvalidConnection.
Направление relay
Чистый модуль examples/apps/relay/direction.liza хранит head, tail, eof,
fin и проверяет переходы. Данные находятся в отдельном региональном буфере.
Ожидающая очередь — диапазон [head, tail); выполняется
0 <= head <= tail <= 2048. Read дописывает в tail, write продвигает head.
После полного опустошения оба индекса сбрасываются в ноль.
Буфер не уплотняется и не является ring buffer. После достижения tail=2048 чтение возобновится после полного опустошения, даже если часть префикса уже отправлена. Это консервативная политика с определённой стоимостью и без memcpy. Модуль отклоняет неверные размеры read/write и преждевременный shutdown через Result, не допуская переполнения индексов.
Verified Relay R1 отдельно проверяет восемь функций этого модуля через фактический Semantic IR для всех входов. Это доказательство координатных переходов, не сохранности байтов в сетевом буфере.
Для каждого направления отдельно рассматриваются последовательности:
- R — байты успешных read;
- W — байты, принятые целевым локальным сетевым стеком через успешные write;
- Q — ещё не отправленные байты буфера.
Контракт успешных шагов: R = W ++ Q. Read добавляет одинаковые байты в R и конец Q. Положительный write переносит префикс Q в W. WouldBlock/Interrupted не изменяют эти последовательности. Успешный write не подтверждает получение данных удалённым приложением.
Два независимых жизненных цикла
На пару есть отдельные forward и reverse. Ожидание, заполнение очереди или EOF одного направления не закрывает другое. Каждый оборот выполняет ограниченное число операций для каждой пары; внутреннего write-all или ожидания connect нет.
При EOF источник больше не читается. Когда его Q пуст и целевой сокет Connected, вызывается shutdown_write на цели. FIN не передаётся раньше накопленных данных. Полное закрытие пары происходит после успешного FIN обоих направлений.
Ключевой сценарий: клиент передал запрос и сделал shutdown(write); proxy досылает запрос, передаёт FIN upstream, продолжает читать его ответ, досылает ответ клиенту и только после обратного EOF закрывает оба сокета. Обратный порядок half-close также поддерживается: EOF от upstream не мешает клиенту продолжать отправлять ему данные.
Во время Connecting клиент может заполнить свою очередь. Если есть место, можно заметить и сохранить EOF ещё до успешного connect. Если очередь заполнена, EOF будет замечен после освобождения места. После Connected данные досылаются, затем передаётся FIN. Fatal error любого направления немедленно завершает всю пару; накопленные байты могут быть потеряны, равенство конечных потоков не обещается.
Backpressure и память
Один регион и один Buffer создаются до event loop: 32768 байтов.
Для пары i область forward — [4096*i, 4096*i+2048), reverse — следующие
2048 байтов. Всего восемь пар, по два независимых диапазона. Reactor имеет
16 слотов для клиентских и исходящих сокетов; listener учитывается отдельно.
Заполненный хвост очереди отключает интерес к чтению соответствующего источника. Пустая очередь отключает интерес к записи цели. Исключения — Connecting, когда нужно проверять завершение connect, и ожидающий shutdown после EOF, если его системный вызов потребовал повторения. Интересы двух направлений объединяются для каждого сокета. Readiness остаётся подсказкой, WouldBlock нормален после poll.
Read пишет непосредственно в диапазон, из которого последующий write берёт байты. Между прикладными стадиями payload не копируется; нет buffer.update, уплотнения, reserve или создания новых пользовательских буферов в event loop. Это не обещание kernel zero-copy. Стек, метаданные reactor/региона/пар и память сетевого стека ОС не входят в 32 КиБ. После закрытия пары её диапазоны можно переиспользовать: логические индексы сбрасываются, старые байты не отправляются.
Проверки
tests/test_proxy.py проверяет O0/O2 и точное совпадение бинарных потоков:
оба порядка half-close, полные ответы после EOF запроса, удерживаемый connect
с пустым и заполненным буфером, восемь пар и повторное использование места,
отказ подключения и reset каждой стороны. Большие потоки передаются одновременно
в обоих направлениях, с разными размерами и скоростями чтения.
Fault runtime ограничивает read до 13 байтов, write до 7, вставляет WouldBlock после readiness и позволяет удерживать Connecting. Отдельный C-тест проверяет pending при SO_ERROR=0 без readiness, сохранение ошибки, запрет I/O до Connected, идемпотентный shutdown_write и stale/foreign ID. Проверяются также чистые переходы координат и отсутствие вызовов выделения payload в relay-функции.
Отдельный математический эксперимент
python -m pip install -r verification/requirements.txt
python -m verification.relay_model.check --output build/relay-model/report.json
Модель отдельно доказывает 9 SMT-обязательств: начальное пустое состояние, сохранность и границы после read/write, допустимость индексной арифметики, EOF, неизменность при WouldBlock, условие FIN и равенство R=W при нормальном завершении. Шесть отрицательных контролей проверяют потерю, дублирование, перестановку байтов, перезапись очереди и преждевременный FIN.
Это индуктивные обязательства над вручную заданной математической моделью, с символическими последовательностями и очередью до 2048 байтов. Они не проверяют фактический Semantic IR, LLVM IR, реализацию Liza-модуля или runtime. Связь модели с исполняемым relay пока подтверждается тестами, не доказательством. Предполагаются корректные read/write, отсутствие aliasing между направлениями и однопоточное исполнение; завершение и доставка удалённому приложению не доказываются.
Отчёт содержит границы, доверенную базу, версию Z3 и SHA-256 модели;
program_verified, runtime_verified, end_to_end_verified остаются false.
Unknown или пропущенный отрицательный контроль не дают passed.
Эксперимент имеет отдельный workflow и не расширяет V4 или общий pipeline V0–V4.
Ограничения
Нет TLS termination, DNS, публичной привязки, балансировки, повторного connect, idle/connect deadlines или остановки по сигналу. Попытка connect ограничена тайм-аутами ОС, а не прикладным deadline. Зависшие пары могут занимать все восемь мест. Это bounded loopback-прототип, не эксплуатационно готовый публичный proxy. Verification Bundle V1 остаётся независимым направлением.