Перейти к содержанию

Verified Relay R2-C — Event Loop Invariant Closure

Статус: первый срез реализован; PR #12 слит. Проверяются 290 обязательств (включая повторную проверку 58 обязательств R2-B), восемь мутаций исходника и независимые конкретные трассы. Это условное индуктивное замыкание для одной выбранной пары прокси 0.0.30, включая оба направления и повторное использование её слота. Проверка всех восьми пар как единой системы, прогресс обслуживания и завершение сервера — отдельно.

Исходная программа и граница

Основа — examples/apps/liza_proxy.liza на коммите 05dcc9c1c8c2166454d2c4064b2a7c3401c6b095 и неизменённый модуль examples/apps/relay/direction.liza. Проверяется фактически полученный Semantic IR; storage_contract и may_trap не являются аксиомами исполнения. Будущие изменения CLI и deadlines в 0.0.31 потребуют отдельного переноса и повторной проверки. Совпадение имени функции не переносит доказательство.

R2-B использует входы после phi и проверяет шесть отдельных участков exchange. R2-C восстанавливает значения этих входов из предшествующего CFG, а выходы — провести через pairs[i] к следующей итерации. Локальные обязательства R2-B заново исполняются на том же сохранённом IR. Дополнительные обязательства R2-C устанавливают сохранение Direction и ID включая терминальные ветви, монотонность EOF/FIN и невозможность возобновить alive=false. Структурная проверка связывает реальные выходные SSA-значения одного участка со входами следующего. Чтение старого report.json само по себе не является такой проверкой.

Состояние одной пары

Выбирается символический индекс i из [0,8). Ему принадлежат участки [4096*i,4096*i+2048) и [4096*i+2048,4096*i+4096) общего буфера из 32768 байтов. Для остальных слотов используется явный frame-контракт: они не меняют выбранную запись и её участки. Проверки сохранения таблицы проводятся для одного активного слота и остальных неактивных записей; это не доказательство произвольного сочетания восьми активных пар. Доказательство этого контракта для полного многоклиентского цикла не входит в первый срез.

Состояние включает запись таблицы, локальный Pair, буфер, логическое поколение пары, два идентификатора соединений и состояние абстрактного reactor. Для каждого направления ведутся математические истории R и W произвольной конечной длины. Истории относятся к конкретному поколению пары, а не просто к индексу массива. Старые байты могут физически оставаться в буфере после закрытия; при пустой новой очереди они не входят в новую историю.

Для живой пары требуется:

Valid(forward) && Valid(reverse)
Valid(d) = 0 <= d.head <= d.tail <= 2048
           && (d.fin => d.eof && d.head == d.tail)
R_forward = W_forward ++ B[4096*i+forward.head : 4096*i+forward.tail]
R_reverse = W_reverse ++ B[4096*i+2048+reverse.head : 4096*i+2048+reverse.tail]

Дополнительно оба ID различны, принадлежат одному reactor и актуальны; Pair.connected согласован с фазой upstream. Forward может принять данные клиента до завершения connect, но отправка upstream и reverse I/O требуют подключения. FIN относится к записи в сокет назначения, а EOF — к чтению из источника; завершение одного направления не закрывает второе.

Неактивная запись имеет оба None, connected=false и два пустых Direction. Состояние с одним Some не считается допустимой записью таблицы. Временное владение принятым client до результата connect моделируется отдельно: ошибка connect должна привести к попытке его отключения без публикации пары.

Обязательства над фактическим IR

Участок Необходимый результат
empty_pair, array.repeat Начальная таблица неактивна, оба направления пусты
Выбор свободного слота Публикация не перезаписывает живую пару; индекс в границах
Accept/connect Публикуются именно полученные ID; новая эпоха и пустые истории
Ready/finish_connect Согласованная фаза сохраняется; ошибка не превращается в успешное подключение
Шесть участков R2-B Предусловия выведены из текущего состояния; результат одного перехода становится входом следующего
pairs[i]=copy pair Сохраняется обновлённое значение в правильном слоте; остальные записи неизменны
Чтение таблицы и phi на backedge Следующая обработка получает сохранённое состояние, а не старое SSA-значение
Disconnect/reset После завершения обработки старые ID больше не используются; запись становится пустой
Повторная публикация Новая эпоха не наследует координаты, EOF/FIN или историю предыдущей

Нормальное завершение пары требует FIN обоих направлений, пустых очередей и R=W в каждой истории. При фатальной ошибке сохранность до ошибки не превращается в обещание досылки: очередь может быть отброшена. В математической композиции терминальная история не переписывается как успешная передача: остаток очереди может быть потерян. Прикладной журнал числа потерянных байтов в этом эксперименте не реализован. Ошибка disconnect не доказывает физическое освобождение сокета; отдельно проверяются порядок вызовов и запрет дальнейшего использования ID при явно указанном контракте runtime.

Индукция и согласованность окружения

Доказательство состоит из установления инварианта, сохранения каждого поддержанного перехода и проверки каждого объявленного обратного ребра. Несколько конкретных оборотов цикла служат replay, но не доказательством индуктивного замыкания. Нельзя заново предполагать корректный Pair, пустую историю или живой сокет на каждом cutpoint.

Абстрактное окружение отслеживает создание, подключение, EOF, shutdown и инвалидацию ID на всей трассе. После успешного shutdown нельзя допускать успешную запись ненулевого диапазона в тот же сокет. После disconnect нельзя выдавать этому ID успешный I/O. Readiness остаётся подсказкой; WouldBlock и Interrupted допустимы по объявленным контрактам.

Для lifecycle-вызовов poll, accept, connect, ready, finish_connect, interest и disconnect модель включает все 12 вариантов ReactorError; реальное тело retry определяет, какие ветви продолжаются. Для байтовых вызовов сохраняется более узкий контракт R2-B: успех, WouldBlock, Interrupted, терминальная Other и явно проверяемая ошибка диапазона. Обобщение на остальные байтовые исходы не подразумевается.

При disconnect действительный логический ID считается потреблённым даже при ошибке закрытия. Это предположение о runtime, а не доказательство реального закрытия ОС. Fatal byte I/O прекращает гарантии содержимого; предполагается, что само размещение Buffer остаётся живым до release. Внешние main/serve, allocator, диагностика startup и физическая реализация финального reactor_close исключены. Для непроверяемых границ зафиксированы структурные хеши блоков: изменение такой границы даёт unknown.

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

Мутации меняют компилируемый исходник приложения. Для каждого контроля нужны сохранённый IR, контрпример и конкретный replay без Z3:

  • Пропущено сохранение обновлённого Pair в таблице.
  • Сохранено старое значение либо выбран соседний индекс.
  • При создании перепутаны client/upstream.
  • Подключение отмечено успешным при Ok(false).
  • После отключения сохранён старый Pair или пропущен reset направления.
  • При повторном использовании слота сохранён старый EOF/FIN.
  • Закрытие пары выполнено после FIN только одного направления.
  • Продолжающийся путь использует ID после его инвалидации.

Недостаточно получить SAT из ослабленного инварианта. Реальное нарушение подтверждается независимо построенной трассой от допустимой инициализации с согласованными исходами I/O. Это не утверждение, что произвольная абстрактная SMT-модель воспроизведена дословно: отчёт отдельно хранит символическое нарушение и конкретное свидетельство того же мутанта. Невоспроизведённый абстрактный контрпример сохраняется как отдельный диагностический результат, не как установленная ошибка приложения.

Состав доказательства и отчёт

  • Независимый исполнитель проверяет поддержанный CFG настоящего IR.
  • Инициализация, переходы, сохранение таблицы и backedges имеют обязательства.
  • Любой непокрытый переход, таймаут или неизвестная инструкция исключает успех.
  • Исходники, IR, контракты окружения, SMT-запросы, версии, хеши и replay сохранены.
  • Отрицательные контроли обнаружены и воспроизведены; CI Linux/macOS/Windows.
  • R1, R2-A/B, V0–V4 и общий pipeline сохраняют собственные границы гарантий.

Положительный статус относится к одной паре при перечисленных frame- и runtime-предположениях. whole_program_verified, liveness_verified, runtime_verified, llvm_verified и end_to_end_verified остаются false. Поле conditional_inductive_pair_verified устанавливается только при полной матрице, проверенной композиции и восьми подтверждённых контролях. unknown, пропущенное обязательство или неподтверждённый контроль исключают общий успех. Отчёт не является сертификатом для малого проверяющего ядра; символический исполнитель, конкретный replay, композиционная обвязка и Z3 входят в доверенную базу.

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

python -m pip install -r verification/requirements.txt
python -m verification.relay_r2c.check --output build/verified-relay-r2c
python -m unittest verification.relay_r2c.test_model -v

Проверки сохраняют исходники, фактический IR, SMT-LIB, версии инструментов, копии кода проверяющих инструментов и SHA-256 артефактов. Выходной каталог должен быть новым или пустым. Обвязка не читает старые положительные отчёты как основание доказательства.

Отдельный replay не требует Z3:

python -S -m verification.relay_r2c.replay \
  --ir build/verified-relay-r2c/mutations/lost_persistence/semantic.json \
  --output replay.json

Исполняются реальные операции IR, включая таблицу, phi и вызовы Direction. Сокетное окружение сохраняет фазы, EOF/FIN и истории между вызовами. Два поколения пары в положительном replay проверяют конкретный сценарий reuse; неограниченное число оборотов следует из локальных универсальных обязательств и композиции, а не из этих двух исполнений.

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

При новой эпохе координаты и логические истории пусты; старое физическое содержимое Buffer не требуется обнулять. Свежесть ID опирается на явный контракт reactor. Из этого не следует доказательство его generational-ID реализации или отсутствия исчерпания поколений.