Verified Relay R2 — Byte Conservation
R2 разделён на два самостоятельных шага с разными границами доверия. R2-A реализует математическую модель буфера, не проверку приложения. Первый срез R2-B — условная проверка отдельных переходов фактического Semantic IR TCP-прокси, отдельно от R2-A.
R1 уже проверяет реальные функции Direction на полном пространстве входов. R2-A не расширяет эту гарантию на байты приложения: это отдельное индуктивное доказательство для независимо написанных переходов. R1, V0–V4, исходный proxy и общий verification pipeline не меняются.
R2-A: состояние и инвариант
Для одного направления состояние:
S = (R, W, B, head, tail, eof, fin)
0 <= head <= tail <= 2048
R = W ++ B[head:tail]
fin implies (eof and head == tail)
R — история успешно принятых байтов. W — история байтов, принятых
целевым локальным сетевым стеком; это не подтверждение получения удалённым
приложением. B — буфер вместимостью 2048 байтов. Модель не уплотняет очередь:
запись идёт в tail, отправка начинается с head, после полного опустошения
оба индекса обнуляются.
Последовательность представлена длиной и отображением целого индекса в
восьмибитное значение. Истории имеют произвольную неотрицательную математическую
длину; она не ограничена u32 или числом итераций. Только count ограничен
диапазоном u32, а доступ к B — диапазоном [0,2048).
Содержимое вне текущей очереди произвольно. Это математическая модель байтов,
не доказательство инициализации физической памяти или allocator.
Равенство последовательностей проверяется по длинам и всем значениям байтов:
rlen = wlen + tail - head
для любого 0 <= p < rlen:
R[p] = W[p], если p < wlen
R[p] = B[head + p - wlen], иначе
Индекс p остаётся свободным символом SMT-запроса. Отсутствие контрпримера доказывает равенство для любой позиции, а не для выбранного набора индексов. Начальное состояние и сохранение инварианта на каждом допустимом переходе дают индуктивную гарантию для любого конечного префикса успешного исполнения. Завершение потока или fairness не доказываются.
Переходы
| Переход | Предусловие и эффект |
|---|---|
| Положительный read | Нет EOF; 0<n<=2048-tail. В B[tail:tail+n] записываются ровно входные байты, остальные байты B неизменны; они же дописываются в R |
| Положительный write | 0<n<=tail-head. В W дописывается ровно B[head:head+n], B и R неизменны; head продвигается на n |
| Опустошение | После write последнего байта head и tail становятся нулём; переданные байты сохраняются в W |
| WouldBlock | B, R, W, координаты и флаги неизменны |
| EOF | Нулевой read при положительной доступной вместимости: меняется только eof |
| FIN | Только после EOF, при пустой очереди и отсутствии прежнего FIN; меняется только fin |
Полный буфер запрещает новый read, даже после частичной отправки префикса. Чтение возобновляется после полного освобождения очереди. EOF не удаляет неотправленные байты; FIN не выдаётся до их передачи.
Ошибка вне WouldBlock завершает доказанный успешный участок исполнения. Модель не предполагает отсутствие побочных эффектов при произвольном Err, не доказывает освобождение ресурсов и не обещает доставку оставшейся очереди. Контракт освобождения сокетов — отдельная задача.
Что проверяет SMT
Итого 34 положительных обязательства:
- Начальные координаты и байтовый инвариант — два обязательства.
- Для каждого из пяти переходов — шесть: состояние, байтовая сохранность, точное изменение B и сохранение остальных байтов, история R, история W, границы фактического диапазона доступа.
- После успешного FIN — равенство длин и всех байтов R/W, два обязательства.
В запросах сохранения полный старый байтовый инвариант используется только
в наблюдаемой позиции p. Это ослабление предусловия: доказательство при
таком предусловии достаточно и для любого полностью корректного состояния.
Оно не означает, что произвольная SMT-модель с sat автоматически описывает
полностью корректную историю.
Поэтому для отрицательного контроля восстанавливается целая история
R := W ++ B[head:tail], проверяется полный конкретный инвариант и отдельно
исполняется переход над списками байтов, без Z3. Невоспроизводимое свидетельство
остаётся unknown. Конкретный replay ограничивает длину W 16384 байтами;
этот технический лимит не применяется к положительным доказательствам.
Превышение лимита не превращается в подтверждённый дефект.
Отрицательные контроли
Одиннадцать мутаций меняют математические переходы, не Liza-код:
| Мутация | Проверяемый дефект |
|---|---|
| Read начинается с tail+1 | Неверный диапазон или выход за границу |
| Read начинается с head | Перезапись ожидающих байтов |
| Read меняет бит входного байта | Подмена содержимого при правильных длинах |
| Read разрешён при полном B | Доступ за пределами 2048 байтов |
| Write читает от tail | Отправляется другой диапазон |
| Write переставляет первые два байта | Нарушение порядка при правильных длинах |
| Write продвигает head на лишний байт | Потеря ожидающего префикса |
| После полного write сохраняется старый tail | Некорректный сброс очереди |
| WouldBlock меняет байт B | Скрытый побочный эффект |
| EOF обрезает очередь | Потеря неотправленных байтов |
| FIN разрешён при непустой очереди | Преждевременное завершение направления |
Все контроли должны давать конкретно воспроизводимое нарушение. Любой
unknown среди выполняемых запросов исключает общий успех. Ошибка модели
не объявляется ошибкой настоящего прокси или сетевого runtime.
Запуск и артефакты
Из корня репозитория в окружении с verification/requirements.txt:
python -m unittest verification.relay_r2a.test_model -v
python -m verification.relay_r2a.check --output build/verified-relay-r2a
Каталог вывода должен быть новым или пустым. --timeout задаёт положительный
лимит одного запроса в миллисекундах, по умолчанию 10000.
Сохраняются исходники модели, контрактов, конкретного replay и тестов,
закреплённые зависимости, SMT-LIB каждого запроса, исходные SMT-результаты,
свидетельства и конкретные байты до/после переходов. report.json содержит
версии Python/Z3, предположения, границы проверки и SHA-256 артефактов,
включая отдельный results.json. Сам отчёт не подписан, не хеширует сам себя
и не является сертификатом доказательства или Verification Bundle.
Отдельный workflow выполняет полный R2-A на Linux, macOS и Windows.
В отчёте model_byte_conservation_verified относится только к модели.
Поля program_verified, semantic_ir_verified, runtime_verified,
llvm_verified, end_to_end_verified, proof_certificate остаются false.
Доверенная база: написанные вручную модель и контракты, представление равенства последовательностей через индексы, Python, SMT-обвязка и Z3. Конкретный replay входит в доверенную базу подтверждения мутаций.
R2-B: отдельный этап
Первый срез R2-B реализует проверку шести ациклических участков с одним I/O-вызовом на путь. Ниже сохранён контракт направления; композиция переходов и весь event loop остаются за границей первого среза.
R2-B должен связать модель с фактическим Semantic IR liza_proxy.liza:
аргументами read/write, результатами I/O, вызовами Direction и физическими
диапазонами общего регионального буфера. Этого R2-A не проверяет.
В приложении восемь пар и шестнадцать участков. Для пары p:
forward_base=4096*p, reverse_base=4096*p+2048; при нумерации направлений
это base(i)=2048*i, 0<=i<16. R2-B должен независимо проверить отсутствие
пересечений, границы в 32768 байтах и checked-арифметику этих смещений.
Предположения о runtime должны быть опубликованы отдельно от доказанных свойств программы:
| Граница | Предположение для условного доказательства |
|---|---|
| Read Ok(n) | 0<=n<=requested; ровно n входных байтов записано в переданный диапазон, остальная память не изменена |
| Write Ok(n) | Для непустого запроса 0<n<=requested; принят ровно префикс переданного диапазона, память не изменена |
| WouldBlock | Нет скрытого переноса или изменения памяти |
| Readiness | Не гарантирует успешный следующий I/O |
| Shutdown Ok | Не меняет байты; обязанность программы — вызывать только после EOF и опустошения очереди |
| Фатальный Err | Успешная трасса прекращается; дальнейшая доставка и отсутствие побочных эффектов не обещаются |
Текущий proxy считает Interrupted и Full повторяемыми исходами вместе
с WouldBlock. R2-A не проверяет эту классификацию runtime-ошибок.
В R2-B для каждого действительно возможного повторяемого исхода потребуется
явный контракт отсутствия скрытого переноса, либо такой путь останется вне
доказанного фрагмента. Нельзя автоматически приравнять произвольный Err
к неизменившемуся состоянию.
Отрицательные контроли R2-B должны менять настоящий Liza-код: неверную половину/базу буфера, tail вместо head, лишний байт при короткой записи, read полного участка, ранний FIN и перезапись соседнего направления. Свидетельства воспроизводятся по фактическому IR при согласованных результатах I/O в поддерживаемых отдельных переходах. Это не закрывает доказательство произвольных последовательностей событий.
Ни один из двух этапов не устанавливает сквозную гарантию для бинарника: LLVM lowering, машинное исполнение, ОС и сокетный runtime остаются за её пределами.