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

Воспроизводимый verification pipeline

Первый общий pipeline запускает неизменённые V0–V4 и объединяет их артефакты, команды и результаты. Он не проверяет произвольный исходник и не создаёт сквозного доказательства от программы до машинного бинарника. Новый инструмент — обвязка существующих экспериментов, а не V5 или новая версия языка.

Что сохраняет запуск

В новом каталоге результатов создаются:

source/                    снимок компилятора, экспериментов и спецификаций
source-manifest.json        SHA-256 и размеры файлов снимка
stages/v0/...              stdout, stderr, исходный report.json и артефакты V0
stages/v1/...              те же материалы V1
stages/v2/...              те же материалы V2
stages/v3/...              калибровка Alive2 и конкретные пары LLVM IR
stages/v4/...              ресурсная модель, мутации и контроли сводок
report.json                общий отчёт со ссылками на исходные результаты
manifest.json              SHA-256 и размеры файлов всего набора

Эксперименты исполняются из снимка, а не из изменяемой рабочей копии. После запуска проверяется неизменность снимка и исполняемых файлов выбранных инструментов. Снимок включает исходники спецификаций, моделей и отрицательных контролей, а не только пользовательские .liza-файлы.

Общий отчёт фиксирует платформу, Python, команды, рабочие каталоги, контролируемые переменные окружения, бюджеты времени, версии из сырых отчётов и хеши инструментов. Полное окружение процесса не сохраняется, чтобы не включать в артефакты посторонние секреты. Git HEAD и признак изменённой рабочей копии — вспомогательные сведения; точные входы определяет хешированный снимок.

Каталог результатов должен быть новым или пустым. Старый report.json не может случайно превратить неудачный повторный запуск в успешный.

Полный запуск

Нужны Python с зависимостями verification/requirements.txt, Clang для V0–V2 и совместимая инструментальная цепочка V3. Подготовка Alive2 и её ограничения описаны в V3. Pipeline ничего не устанавливает самостоятельно.

python -m verification.pipeline \
  --output build/verified-pipeline \
  --clang /path/to/core-clang \
  --v3-clang /path/to/llvm/bin/clang \
  --alive-tv /path/to/alive2/build/alive-tv \
  --alive-source /path/to/alive2 \
  --llvm-config /path/to/llvm/bin/llvm-config \
  --opt /path/to/llvm/bin/opt \
  --llvm-revision YOUR_RECORDED_LLVM_REVISION \
  --z3 /path/to/z3 \
  --toolchain-lock verification/v3/toolchain-lock.json

Пути в примере требуется заменить на своё окружение. Существующий lock V3 описывает конкретный macOS ARM64 toolchain; он не является универсальным lock для всех ОС. Без --toolchain-lock сохраняются версии и хеши, но не утверждается соответствие зафиксированному набору V3.

Clang разделён на два параметра намеренно. В локальной проверке системный Clang успешно обработал V0–V2, а LLVM 23.1.4 использовался для V3. Попытка запустить V2 с LLVM 23 дала unknown из-за неподдержанной группы атрибутов O2 IR. Pipeline сохранил этот результат; исходный IR и замороженная модель не переписывались ради успеха.

V3 всегда запускается с --actual: одной калибровки недостаточно для общего успеха. Если Alive2 или необходимые параметры отсутствуют, V3 отмечается как unknown, а полный запуск остаётся неполным. Другие этапы продолжаются, чтобы сохранить полезные результаты и диагностику.

Полнота и исходы

Обвязка проверяет ожидаемые матрицы текущих экспериментов: 40 обязательств V0, 32 V1, 74 V2, 90 реальных сравнений V3 вместе с калибровкой и матрицу V4 из 11 положительных программ, 7 мутаций и 8 контролей сводок. Числа не являются мерой общей корректности: они служат проверкой полноты конкретного набора. Пустые и дублирующиеся строки не дают успеха.

Сверяются также имена субъектов и этапов, заявленные хеши артефактов и моделей. Общие хеши вычисляются поверх фактически сохранённых файлов. Успешный код завершения дочернего процесса без корректного полного отчёта недостаточен.

Общий статус Смысл Exit code
passed Все пять экспериментальных матриц и их контроли прошли 0
partial Выбранное подмножество прошло, другие этапы явно не запускались 2
incomplete Хотя бы один выбранный этап не прошёл, не поддержан или не завершился 1

passed относится к запуску экспериментов. Он не означает доказательства всех программ, полной корректности компилятора или машинного backend.

В общем report.json успех запуска отделён от сквозной верификации:

{
  "pipeline_status": "passed",
  "end_to_end_verified": false
}

pipeline_status принимает значения из таблицы выше. Поле status сохранено как совместимый синоним и всегда совпадает с pipeline_status. end_to_end_verified всегда равно false, включая полностью успешный запуск V0–V4: обвязка не строит сквозного доказательства. Эти поля сохраняются также в промежуточных, частичных и неполных отчётах.

Поле verification_scope указывает на область свойств каждого этапа (stages.<stage>.coverage_contract), его спецификацию, исходные предположения и исключения (scope). Контракт описывает запрошенную область проверки; только статус passed этапа подтверждает прохождение соответствующей матрицы. Перечисление свойств не превращает пропущенный или неуспешный этап в доказанный.

Каждый дочерний отчёт сохраняется без изменения. В общем отчёте есть индекс его исходных статусов с путём к соответствующему полю:

  • proved относится к доказанному свойству в модели; verified V3 — к LLVM refinement, а verified_fragment V4 — к поддержанному ресурсному фрагменту.
  • Контрпример к индуктивному обязательству остаётся неподтверждённым дефектом исполнения, пока нет конкретного replay.
  • Подтверждённое нарушение ресурсной модели и подтверждённая недостаточность сводки возврата различаются. Последняя не объявляется автоматически уязвимостью освобождения памяти.
  • unknown и unsuitable сохраняются; пропущенный этап имеет not_selected.

Ожидаемый unknown в специальном отрицательном контроле проверяет отказ инструмента от неподдержанной конструкции. Его роль помечается отдельно: это не успешно доказанное свойство программы. Аналогично ожидаемые контрпримеры мутаций не выдаются за дефекты исходного компилятора.

Частичный запуск и проверка сохранённого набора

Быстрая проверка без LLVM/Alive2:

python -m verification.pipeline --stages v4 --output build/pipeline-v4

Успешный частичный запуск возвращает 2, а не 0. Для V0/V1/V2 требуются Z3 и подходящий Clang. --stage-timeout задаёт предел всего дочернего этапа, --solver-timeout-ms — SMT-запроса V0–V2, --alive-timeout — сравнения V3. Таймаут сохраняется в отчёте, дочерние процессы завершаются; он не является контрпримером к программе.

Проверка целостности уже сохранённых материалов:

python -m verification.pipeline --check-bundle build/verified-pipeline

Эта команда сверяет файлы с manifest.json, включая сам общий отчёт, и сообщает записанный статус запуска. Она не повторяет доказательства. Манифест не подписан: совместная подмена файлов и манифеста не обнаруживается как нарушение подлинности. Хеши служат идентификации и контролю целостности, не заменяя доверенный источник артефактов.

Для повторного выполнения можно перейти в source/ сохранённого набора и запустить ту же команду с новым каталогом вывода и соответствующими путями инструментов. Сохранённые команды содержат абсолютные пути первоначального окружения; после переноса их нужно сопоставить с новым расположением.

Доверенная база и границы

Pipeline добавляет к доверенным моделям V0–V4 свою обвязку, адаптеры отчётов, снимок исходников и вычисление хешей. Это не уменьшение доверенной базы само по себе. Сырые отчёты сохраняют конкретные предположения, исключения и версии каждого эксперимента; их объединение не доказывает совместимость моделей.

Инструментальные библиотеки, ОС и SDK не упаковываются вместе со снимком. Это воспроизводимый набор входов и команд с явно указанными внешними зависимостями, а не герметичная сборка. Время исполнения и иные изменчивые поля отчётов не обязаны совпадать побайтово.

Общий отчёт не является проверяемым сертификатом доказательства. Он ещё не связывает свойства исходной программы с конечным бинарником. Эта связь и независимые сертификаты остаются следующими исследовательскими задачами. Обычная сборка Liza не требует запуска pipeline или SMT-решателя.

CI

Автоматические push/PR-проверки обвязки идут на Linux, macOS и Windows. Они включают тесты отказов и настоящий частичный запуск V4; это не означает полного запуска V0–V4 на всех трёх платформах. Полная матрица pipeline предусмотрена отдельным macOS-job по workflow_dispatch с full=true и проверкой lock V3. Независимые workflows V0–V4 продолжают работать отдельно.