Liza Verified V0: первый эксперимент

Экспериментальное направление, отдельно от версии языка 0.0.25. Цель — проверять соответствие реализации определённой семантике Liza. Первый эксперимент охватывает десять конкретных функций над u8 и i8. Он не означает, что весь компилятор или произвольная программа формально верифицированы.

Что проверяется

Для каждого типа проверяются сложение, вычитание, умножение, последовательность (x + 1) - 1 и условное вычисление x + 1. Входы — все битовые представления параметров, включая оба значения bool. Это символическая проверка всего конечного пространства входов этих функций, а не выборка случайных тестов.

Контракт checked-арифметики:

Если математический результат представим, возвращается его точное значение.
Если результат не представим, выполнение достигает обязательного trap.
Trap промежуточной операции нельзя устранить ради конечного результата.
Неисполняемая ветвь не вычисляется.

Например, sequence_u8(255) должен завершиться trap, хотя при остальных входах функция возвращает исходное значение. branch_u8(255, false) должен успешно вернуть 255.

// Fixed verification subjects. Specifications live separately in reference.py.
fn add_u8(x:u8,y:u8)->u8 { return x+y }
fn sub_u8(x:u8,y:u8)->u8 { return x-y }
fn mul_u8(x:u8,y:u8)->u8 { return x*y }
fn add_i8(x:i8,y:i8)->i8 { return x+y }
fn sub_i8(x:i8,y:i8)->i8 { return x-y }
fn mul_i8(x:i8,y:i8)->i8 { return x*y }
fn sequence_u8(x:u8)->u8 { return (x+1)-1 }
fn sequence_i8(x:i8)->i8 { return (x+1)-1 }
fn branch_u8(x:u8,take:bool)->u8 { if take {return x+1} return x }
fn branch_i8(x:i8,take:bool)->i8 { if take {return x+1} return x }
fn main()->u32 {return 0}

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

Четыре проверки каждой функции

Представление	Утверждение
Semantic IR	Соответствует независимому контракту функции
Сгенерированный LLVM IR	Сохраняет значение и обязательный trap
LLVM IR после O0	Соответствует тому же контракту
LLVM IR после O2	Соответствует тому же контракту

Получается 40 обязательств. Каждый запрос ищет вход, на котором результат, наличие trap или определённость исполнения расходятся со спецификацией. unsat означает отсутствие такого входа в принятой модели. Эквивалентность представлений следует из их соответствия общему контракту.

Допустимый фрагмент не содержит I/O, аллокаций, памяти и пользовательских вызовов. Это проверяется разрешённым набором инструкций, а не только аннотацией pure. Циклы, рекурсия и неизвестные операции не поддерживаются.

Результаты и границы доверия

Статус	Значение
`proved`	Z3 установил отсутствие контрпримера в модели
`counterexample`	Найден конкретный вход, нарушающий контракт
`unknown`	Неподдерживаемый IR, таймаут или другая неопределённость

unknown никогда не считается успешной проверкой. Ошибка запуска инструмента также приводит к неуспеху. Сохранённые SMT-LIB файлы — запросы поиска контрпримеров, не сертификаты доказательств.

Доверенная база первого эксперимента:

Независимые формулировки контрактов.
Парсер и символическая модель выбранного фрагмента IR, генератор запросов.
Z3, Python и среда их исполнения.

Модель LLVM пока мала и сама не верифицирована. Достижимое создание poison через nsw/nuw консервативно считается нарушением, даже если значение затем не используется. Атрибут диапазона возвращаемого значения проверяется, а не принимается как предположение. Достижимый unreachable без trap — ошибка.

Доказательство относится к конкретным сохранённым IR, а не ко всем возможным выходам компилятора. Машинный код, ABI, linker, ОС, время выполнения, ownership и зависимости регионов пока за пределами проверки. Проверка на трёх ОС показывает воспроизводимость эксперимента с их LLVM; она не доказывает корректность трёх машинных backend.

Как проверяется сам инструмент

В отдельные копии сгенерированных функций намеренно внесены ошибки: удалённая и инвертированная проверка переполнения, неверная операция, неверная знаковость, устранённый промежуточный trap, принудительное выполнение невыбранной ветви, poison вместо trap. Отдельно меняется операция Semantic IR.

Все восемь контрольных поломок должны получить counterexample. Для удаления промежуточного trap найден вход x = 255. Неизвестный вызов должен получить unknown.

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

Воспроизведение

Z3 нужен только этому эксперименту, обычная сборка Liza от него не зависит.

python3 -m venv build/verified-env
build/verified-env/bin/python -m pip install -r verification/requirements.txt
build/verified-env/bin/python -m unittest verification.test_verifier -v
build/verified-env/bin/python verification/check.py --output build/verified

На Windows используется build\verified-env\Scripts\python.exe. Нужен Clang в PATH; другой путь задаётся через --clang. --timeout-ms задаёт положительный лимит времени каждого запроса, по умолчанию 10000 мс.

Отчёт report.json содержит статусы, контрпримеры, версии Z3 и Clang, границы доверия и SHA-256 артефактов. Вместе с ним сохраняются исходник, Semantic IR, LLVM IR, намеренно испорченные примеры и SMT-LIB запросы. Отдельный CI Liza Verified (experimental) запускает эксперимент на Linux, macOS и Windows и сохраняет эти артефакты.

Дальнейшее направление

Следующие кандидаты — проверки границ, более широкий фрагмент control flow, а затем инварианты потокового UTF-8 и поколений идентификаторов таблицы. Расширение области доказательства требует расширения и проверки модели, а не только добавления новых примеров.

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

Семантика LLVM сверяется с LLVM Language Reference. Решатель: Z3.

Продолжение: V1 — Bounds and Control Flow. Исходники, спецификации и тесты V0 сохранены без изменений; V1 проверяется отдельно.