Verified Relay R2-B — Semantic IR Byte Binding

Первый срез R2-B связывает координаты Direction, диапазоны общего буфера и результаты сокетного I/O в фактическом Semantic IR liza_proxy.liza. Проверяются шесть ациклических участков: read, write и FIN для forward/reverse. Каждый участок содержит не более одного I/O-вызова на исполняемом пути.

58 обязательств, восемь компилируемых мутаций исходника с конкретным replay, 28 тестов проверяющего инструмента. R2-A остаётся отдельной математической моделью. Прокси, Direction, язык и runtime не изменены; R1, V0–V4 и общий verification pipeline не расширяются.

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

Что связывается

Для пары slot из [0,8):

forward_base = 4096*slot
reverse_base = 4096*slot + 2048
общий буфер: 32768 байтов
R = W ++ B[base+head:base+tail]

Верификатор исполняет реальные mul, add, чтения полей и вызовы из IR. Смещение в модели I/O берётся из вычисленного аргумента вызова, а не подменяется ожидаемым base+head или base+tail.

Проверяется:

Вызов выполняется ровно при разрешающем условии: alive, готовность/подключение, доступное место или ожидающий префикс, а для FIN — EOF и пустая очередь.
Read использует источник соответствующего направления, смещение base+tail и размер 2048-tail; write — соответствующего адресата, base+head и tail-head.
Диапазон остаётся внутри своего 2048-байтового участка и общего буфера.
Возвращённый count проходит через настоящий Result и действительные вызовы Direction; состояние изменяется именно на это число байтов.
При коротком write отправляется правильный префикс, неотправленный суффикс сохраняется. При полном write координаты сбрасываются без потери истории W.
Read изменяет ровно свой диапазон; все остальные байты общего буфера, включая остальные 15 участков, сохраняются.
WouldBlock и Interrupted не меняют координаты и байты при указанных ниже runtime-предположениях. Readiness не считается обещанием успешного I/O.
EOF не удаляет очередь; FIN не вызывается раньше её опустошения.

Идентичность client/upstream также проверяется: правильные байты, отправленные в неправильное соединение, не считаются корректным переходом.

Истории R/W имеют произвольную математическую длину. Равенство проверяется по длинам и байту в произвольной символической позиции, не конечным перебором буферов. Свойство соседних участков проверяется для произвольных j из [0,16) и позиции из [0,2048), кроме текущего направления.

Точные границы участков IR

Проверка использует явный manifest для текущего Semantic IR версии 20. Это выбранные участки конкретной программы, не автоматический анализ любого event loop. Вход расположен после phi указанного блока; выход — после исполнения phi, до следующего условия. Исходный IR не переписывается.

Участок	Вход	Выход
forward.read	b91	b114
forward.write	b114	b134
forward.fin	b134	b154
reverse.read	b154	b177
reverse.write	b177	b197
reverse.fin	b197	b217

Все шесть read/write/shutdown-вызовов в exchange должны попасть ровно в объявленные участки. Проверяются их CFG, отсутствие обратного ребра, форма входных/выходных phi и внешние SSA-зависимости. Изменённая неподдерживаемая форма или неизвестный вход дают unknown, не автоматический успех. Для каждого запуска сохраняется cut.json с реальными блоками и привязками.

Manifest связывает внешние значения: индекс slot, client/upstream, readiness, reactor, текущий Pair и единственный Buffer. Происхождение ID проверяется по операциям извлечения Some из полей исходного Pair, slot — по индексу чтения массива пар. Установление всех входных отношений на пути от main не доказано. В частности, входные phi принимаются как параметры выбранного перехода; их предшествующие ветви находятся вне этой проверки.

Нужны следующие предусловия:

slot находится в [0,8), оба Direction корректны;
client/upstream — различные действительные соединения данного reactor, согласованные с полями Pair;
существует один живой инициализированный Buffer<u8> размером 32768 байтов; во время перехода никто другой не меняет его;
исходная история удовлетворяет байтовому инварианту текущего направления.

Флаги alive/connected произвольны; readiness и код failure охватывают весь диапазон u32. Перенос владения и тождество view/Buffer моделируются по контракту IR, но самостоятельного доказательства lifetime или allocator здесь нет.

Интерпретация фактического IR

Сохраняются побайтно исходники proxy и Direction; обычный компилятор создаёт полный Semantic IR приложения. Проверяется именно сохранённый JSON.

Интерпретируются CFG, предшественник phi, switch/Result, поля и обновления Pair, copy/move, product unpack, view, checked u32 add/sub/mul, сравнения и битовые маски. Выбранный участок не содержит циклов. Достижимый trap или unreachable не считается успешным исходом.

Тела Direction исполняются неизменённым символическим интерпретатором R1 из этого фактического IR. Готовый отчёт R1 и may_trap/storage_contract не подставляются как аксиомы. retry читается как фактический enum-switch с константными возвратами; неподдерживаемое расширение его тела даёт unknown.

Положительная матрица содержит 56 обязательств по шести участкам и два арифметических обязательства о границах/непересечении 16 участков. Проверка точного смещения реального вызова связывает эти арифметические свойства с исполнением выбранного IR, а не только с отдельно объявленной формулой base.

Assume–guarantee граница I/O

Проверяющий инструмент не исполняет реализацию net-функций. Он применяет нижеуказанные контракты к фактическим аргументам вызовов. Реализация этих контрактов в stdlib, C runtime и ОС остаётся предположением.

Исход	Предположение
Read Ok(n)	Положительный допустимый запрос; `0<=n<=requested`; ровно n входных байтов попадает в переданный диапазон, остальная память неизменна
Write Ok(n)	Положительный допустимый запрос; `0<n<=requested`; принят ровно префикс указанного view, память неизменна
Shutdown Ok	Байтовых эффектов нет; программа обязана предварительно установить EOF и пустую очередь
WouldBlock	Нет скрытого переноса и изменений памяти
Interrupted	То же отдельное предположение об атомарном отказе без переноса
Other	Терминальная ошибка; проверяется переход alive=false, но байтовые эффекты и доставка после ошибки не сертифицируются
Read InvalidRange	Для действительного подключённого stream нулевой или выходящий за буфер запрос отвергается до переноса; приложение прекращает направление

Для каждого read/write проверяется и размер запрошенного диапазона, и соответствие возвращённого count. Один не подменяет другой. Нулевой read означает EOF; нулевой успешный write непустого запроса не входит в принятый контракт прогресса.

InvalidRange используется в контроле ошибочно разрешённого read полного буфера. Его запрос равен нулю, поэтому replay возвращает именно InvalidRange согласно контракту reactor, а не искусственный WouldBlock. У исходного приложения разрешающие условия исключают такой вызов.

Full и остальные варианты ReactorError в первом срезе не моделируются, даже если текущий retry классифицирует некоторые из них как повторяемые. Они не объявляются автоматически эквивалентными WouldBlock или Other.

Мутации настоящего приложения

Изменение исходника	Контрпример
Forward read пишет в другую половину	Изменены байты соседнего направления после Ok
Base read увеличен на единицу	Записан неверный физический диапазон после Ok
Write начинается с tail	В историю W попали другие байты
В Direction.write передаётся count+1	Логическая очередь расходится с фактически принятым префиксом
Read разрешён при заполненной очереди	Реальный I/O-вызов выполнен при запрещённом состоянии
FIN использует valid вместо needs_fin	Преждевременный вызов shutdown
Reverse read пишет поверх forward	Изменён другой участок общего буфера
Forward write использует client вместо upstream	Неверный адресат фактического вызова

Каждый мутант проходит обычную компиляцию. Для байтовых контролей поиск требует успешного переноса и нарушения соответствующего байтового свойства; одного неверного аргумента на пути WouldBlock недостаточно.

Контрпример повторяется отдельным конкретным исполнителем сохранённого IR с согласованными mock-результатами I/O. Конкретные Direction-вызовы исполняет независимый concrete replay R1; Z3 при replay не нужен.

В SMT исходный байтовый инвариант используется в произвольной наблюдаемой позиции. Перед replay восстанавливается полностью корректная история R := W ++ B[base+head:base+tail]. Поиск отрицательных свидетельств ограничивает W 4096 байтами; технический предел replay — 16384. Эти ограничения не применяются к положительным доказательствам. Невоспроизведённый контрпример или timeout дают unknown.

Запуск и артефакты

python -m unittest verification.relay_r2b.test_model -v
python -m verification.relay_r2b.check --output build/verified-relay-r2b

Требуются зависимости verification/requirements.txt; каталог вывода — новый или пустой. --timeout задаёт положительный лимит одного SMT-запроса, по умолчанию 10000 мс.

Пример независимого повторения сохранённого контрпримера без site-packages/Z3:

python -S -m verification.relay_r2b.replay --ir build/verified-relay-r2b/mutations/read_wrong_half/semantic.json --cut forward.read --witness build/verified-relay-r2b/mutations/read_wrong_half/checks/results.json

Сохраняются оригинальные и изменённые исходники, полный фактический IR, manifest участков, SMT-LIB, результаты, конкретные байты в hex и трассы IR. Отчёт фиксирует Python/Z3/IR, предположения, границы и SHA-256 артефактов. В tools находятся исходники компилятора, stdlib и использованных проверяющих модулей. Это воспроизводимые свидетельства, не подписанный сертификат и не новый Verification Bundle. Отдельный workflow выполняет полный срез на Linux, macOS и Windows.

Что остаётся за границей

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

Не проверены установление предусловий от main, accept/connect/poll, публикация обновлённого Pair обратно в массив, весь event loop, произвольные последовательности событий, освобождение ресурсов, allocator, runtime, LLVM и машинный код. Значение conditional_ir_byte_binding_verified=true относится только к выбранным переходам. whole_program_verified, event_loop_verified, runtime_verified, llvm_verified, end_to_end_verified и proof_certificate остаются false.

Следующий самостоятельный срез может установить достижимость этих предусловий и сохранение отношений между соседними переходами. Их композиция в доказательство всего event loop не подразумевается текущим отчётом.