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

Liza Verified V3: LLVM Translation Validation

V3 — отдельный эксперимент проверки LLVM refinement через Alive2. Он не меняет язык, обычную сборку или замороженные наборы V0/V1/V2.

Результат с согласованным целевым окружением

Проверка Результат локального запуска
V3-A: корректные пары 3/3 refinement подтверждены
V3-A: намеренные поломки 7/7 обнаружены
V3-B: исходный LLVM → Clang O0/O2 36/36 refinement подтверждены
V3-B: исходный LLVM → opt default<O0/O2> 36/36 refinement подтверждены
V3-B: Clang O0 → O2 18/18 refinement подтверждены

Итого 90/90 сравнений, без unknown. Отдельные локальные запуски с LLVM 23.1.4 подтвердили эту матрицу для macOS ARM64, Linux x86-64 и Windows x86-64. Последние два запуска — проверка IR для cross-target, а не выполнение Windows/Linux-программ на macOS.

Первый эксперимент имел 54 успешных сравнения и 36 unknown, поскольку backend не задавал target triple и data layout. Его сводка сохранена в verification/v3/initial-results.json. Артефакты того запуска не исправлялись.

Теперь liza.target.resolve получает канонический triple, data layout, размер и выравнивание указателя, выравнивание i32/i64 и порядок байтов от выбранного Clang до генерации модуля. Проба не требует заголовков, линковки или исполнения целевого кода. Для x86-64 явно выбирается -march=x86-64, для ARM64 — -mcpu=generic.

Backend llvm(module, target) записывает окружение при создании IR. emit-llvm, build и run используют этот путь, выбранный --clang и необязательный --target. Clang получает те же параметры; предупреждение о замене triple становится ошибкой. Внутренний вызов llvm(module) без окружения сохраняется для замороженных V0/V1/V2 и существующих инструментов.

Область V3 — 64-битные little-endian цели. Используются обычные указатели address space 0 и стандартное соглашение вызова LLVM C. Полная data layout (включая остальные адресные пространства) сохраняется и сравнивается; новые адресные пространства не появляются в проверяемых функциях. Это не доказательство ABI произвольных внешних функций или runtime.

Для trap → unreachable Alive2 по-прежнему предъявляет x = 255 и диагноз Source is more defined than target.

Инструменты локального запуска: Alive2 a68009c9e81575bdcc249d3cc534514a76112221, Homebrew LLVM/Clang 23.1.4, Z3 5.3.1. Исходники Alive2 не изменены.

Платформенный CI

Workflow verified-v3.yml сначала генерирует и хеширует IR на нативных Linux/macOS/Windows runners. Затем отдельный macOS runner с Alive2 проверяет каждый набор без изменения содержимого модулей. Это проверка IR от трёх платформенных компиляторов, а не запуск Alive2 или машинного кода на каждой ОС.

environment.json сохраняет версию генерировавшего Clang, точные команды, целевое окружение, ABI-пробу и хеши входных артефактов. Отчёт отдельно сохраняет версии инструментов proof runner. Полнота списка функций, неизменность исходников и совпадение метаданных проверяются до валидации. Любой unknown или потерянный контроль приводит к ненулевому коду завершения.

Два этапа

V3-A: Trap Calibration. Сначала проверяется пригодность выбранной сборки Alive2 для обязательных traps Liza. Калибровка содержит корректные пары и намеренно неправильные преобразования. Исходные LLVM-модули не инструментируются: trap не заменяется специальным возвращаемым значением.

V3-B: Actual IR Validation. Только после прохождения всех контролей проверяются точные модули, произведённые Liza для исходников V0/V1, и результат их обработки Clang с O0/O2. Дополнительно сравниваются неизменённые артефакты O0 → O2 с одинаковыми платформенными метаданными. Функция выбирается параметрами Alive2, а модуль сохраняется полностью. main исключён из области проверки.

Отдельный путь opt -passes=default<O0/O2> сохраняет явно заданные метаданные модуля. Он проверен без инструментирования, но не подменяет производственный pipeline Clang. Для каждого пути сохраняется собственная команда и собственные LLVM-артефакты.

Проверяется переход LLVM → LLVM. Корректность lowering Semantic IR → LLVM, машинного кода и произвольных циклов этим экспериментом не устанавливается.

Калибровка

Пара Ожидание
Checked u8 без изменений Refinement
Overflow intrinsic → явное сравнение с 255 Refinement
Удаление overflow check Контрпример
(x+1)-1 → x Контрпример
Trap → достижимый unreachable Контрпример; иначе класс не проверен
Checked add → add nuw, poison в результате Контрпример; иначе класс не проверен
Checked add → add nuw, poison в условии ветвления Контрпример; иначе класс не проверен
После trap: unreachable → ret Refinement: trap не возвращает управление
Bounds: < 4 → <= 4 Контрпример
Запись в исходный снимок вместо копии Контрпример

Последние два контроля запускаются после успешной калибровки traps. Валидный LLVM-блок обязан иметь терминатор: «trap без unreachable» проверяется как вызов llvm.trap с последующим ret, а не как синтаксически незавершённый блок.

Статусы и область утверждения

  • verified: refinement подтверждён, все обязательные контроли эксперимента обнаружены. Это результат в модели Alive2, не доказательство самого Alive2.
  • counterexample: инструмент отверг конкретное преобразование.
  • unknown: timeout, ошибка, неподдерживаемая конструкция, пропущенная функция или неполный отчёт. Не считается успехом.
  • unsuitable: Alive2 принял намеренно неправильное преобразование, существенное для контракта Liza. Это статус нашей обвязки.

Внутренний raw_status = refinement_verified сохраняется отдельно. Успех одной положительной пары не разрешает объявить весь класс проверенным: нужно учитывать итоговый статус калибровки.

Обвязка ожидает ровно один результат для каждой выбранной функции. Нулевой код завершения, отсутствие контрпримеров и частично успешный отчёт не достаточны. Неуспешная калибровка блокирует V3-B и возвращает ненулевой код завершения. Полезный результат unsuitable документируется как ограничение, а не превращается в зелёную проверку.

Доверенная база

Alive2 проверяет refinement LLVM, который в общем случае слабее эквивалентности исходов Return(value) | Trap. Калибровка проверяет важные контрольные случаи, но не доказывает эквивалентность этих отношений для всего LLVM.

Аргументы функций ограничены определёнными значениями Liza: --disable-undef-input --disable-poison-input. Это явное предположение обоих этапов, а не отключение проверки poison, создаваемого внутри функции. Контроли add nuw проверяют именно внутреннее возникновение poison.

Доверенными остаются модель Alive2, перевод LLVM в его внутреннее представление, SMT-решатель и обвязка эксперимента. Независимый инструмент уменьшает зависимость от собственных интерпретаторов LLVM V0/V1; это не автоматическое уменьшение всей доверенной базы.

Alive2 не поддерживает межпроцедурные преобразования. V3 не проверяет произвольный whole-program pipeline и не использует встроенный оптимизатор Alive2 вместо заявленного Clang O2. Проверка относится только к сохранённым парам модулей и перечисленным функциям.

Воспроизводимость

report.json сохраняет SHA-256 обоих модулей каждой пары, исходный вывод Alive2, команды, версию LLVM, идентификатор его сборки, commit Alive2, состояние checkout, хеш исполняемого файла и версию Z3. В метаданных каждого модуля сохраняются target triple и полная data layout; null означает, что директива отсутствует в самом модуле, а не что проверены все платформы.

Отчёт не является независимо проверяемым сертификатом доказательства. Точный commit checkout и хеш бинарника полезны для аудита, но сами по себе не доказывают, что бинарник построен именно из этих исходников.

Исходники инструмента: Alive2. Для повторения нужны отдельно установленные совместимые LLVM, Z3, CMake, Ninja и re2c. Эти зависимости не нужны для обычной сборки Liza.

python3 -m unittest verification.v3.test_verifier -v
python3 verification/v3/check.py \
  --alive-tv /path/to/alive2/build/alive-tv \
  --alive-source /path/to/alive2 \
  --clang /path/to/llvm/bin/clang \
  --llvm-config /path/to/llvm/bin/llvm-config \
  --opt /path/to/llvm/bin/opt \
  --llvm-revision EXACT_SOURCE_REVISION_OR_DISTRIBUTION_BUILD \
  --z3 /path/to/z3 \
  --output build/verified-v3

Флаг --actual включает V3-B после успешной калибровки. --target задаёт цель Clang. --inputs принимает проверяемые артефакты, ранее созданные python verification/v3/prepare.py --output DIRECTORY на другом runner. Артефакты размещаются в build/verified-v3; результаты V0/V1/V2 запускаются и сохраняются отдельно.

Скрипт verification/v3/build.sh собирает закреплённую ревизию Alive2 из чистого checkout. Пример для использованного окружения:

git clone https://github.com/AliveToolkit/alive2 /tmp/liza-alive2
git -C /tmp/liza-alive2 checkout --detach a68009c9e81575bdcc249d3cc534514a76112221
ALIVE_SOURCE=/tmp/liza-alive2 \
LLVM_PREFIX=/opt/homebrew/opt/llvm \
Z3_PREFIX=/opt/homebrew/opt/z3 sh verification/v3/build.sh

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

Сводка первого запуска с хешами пар сохранена в verification/v3/recorded-results.json. Полные исходные выводы Alive2 и копии всех модулей находятся в локальном каталоге отчёта.

Фиксация proof toolchain

verification/v3/toolchain-lock.json фиксирует проверенную сборку macOS ARM64: LLVM 23.1.4, Z3 5.3.1 и используемую библиотеку zstd. Проверяются SHA-256 Clang, opt, llvm-config, библиотек LLVM/Clang, Z3 и zstd. Отдельно зафиксированы digest и адреса исходных Homebrew bottles LLVM/Z3/zstd.

CI устанавливает пакеты-кандидаты, затем до сборки Alive2 проверяет их байты по lock-файлу. Обновление Homebrew, совпадающее имя версии с другим бинарником, отсутствующая библиотека или иной префикс установки останавливают проверку. Верификатор повторяет контроль с --toolchain-lock verification/v3/toolchain-lock.json, сверяет выбранные исполняемые файлы и ревизию Alive2 и сохраняет результат в report.json. Несовпадение даёт unknown, без запуска доказательных обязательств.

Это фиксация исполняемых компонентов proof worker, а не полностью герметичная сборка: ОС, SDK, CMake, re2c и системные библиотеки остаются внешними зависимостями. Доступность старых архивов также не гарантируется. При изменении пакетов нужно восстановить сохранённые артефакты либо явно пересмотреть lock и заново выполнить калибровку. Хеши не обновляются в CI. Нативные Clang-генераторы трёх платформ по-прежнему записывают свои версии в environment.json; они не подменяются proof toolchain.

ABI-проба дополнительно тестируется на ошибках Clang/SDK, отсутствии исполняемого файла, неполном ответе, неподдерживаемой архитектуре/ABI, изменении triple/layout/выравнивания между пробами и использовании wrapper с пробелами в пути. Ошибочные конфигурации не получают молчаливый fallback.

Успех калибровки остаётся эмпирической проверкой пригодности конкретной сборки Alive2; он не доказывает общую эквивалентность traps в полной семантике LLVM.