Liza Verified V2: Loop Invariants

V2 проверяет два алгоритма с параметрической длиной входа: линейный поиск по View<u8> и последовательную сумму View<i32>. Доказательство опирается на индукцию по переходам CFG, а не на разворачивание цикла до некоторого числа итераций.

Длина охватывает весь диапазон u32, включая 0 и 0xFFFFFFFF. Число итераций математически конечно и ограничено типом длины; эксперимент не утверждает поддержку бесконечной длины. Но перебора всех итераций в верификаторе нет: проверяется один произвольный переход между точками с инвариантом.

Наборы V0 и V1 сохранены без изменения исходников, спецификаций и тестов. V2 — отдельный эксперимент, не новая версия языка.

Проверяемые программы

// A missing match is represented by data.len (outside valid indices).
fn search(data:View<u8>,needle:u8)->u32 {
    var i:u32=0
    while i<data.len {
        if data[i]==needle {return i}
        i=i+1
    }
    return data.len
}
fn sum(data:View<i32>)->i32 {
    var i:u32=0
    var acc:i32=0
    while i<data.len {
        acc=acc+data[i]
        i=i+1
    }
    return acc
}
fn main()->u32 {return 0}

search возвращает первое совпадение. При отсутствии совпадения возвращается data.len — значение вне диапазона допустимых индексов. Option в область модели этого эксперимента не добавляется.

sum выполняет сложения в порядке входных элементов. Например, для [2147483647, 1, -1] окончательная математическая сумма помещается в i32, но программа должна завершиться trap при втором сложении.

Инварианты и завершение

Спецификации находятся вне исходного языка. Программисту не нужно писать invariant или новые конструкции Liza.

Для поиска инвариант в заголовке Semantic IR:

0 ≤ i ≤ length
для каждого j в [0, i): data[j] ≠ needle

Для суммы вводятся математические префиксы:

S(0) = 0
S(k + 1) = S(k) + data[k]

Инвариант нормального выполнения:

0 ≤ i ≤ length
acc = S(i)
для каждого k в [0, i]: S(k) представима в i32

Мера завершения для обоих алгоритмов — length − i. На каждом обратном ребре она неотрицательна и строго уменьшается. Остальная часть CFG между точками проверки ациклична. Эти два условия вместе с покрытием путей обеспечивают завершение возвратом либо обязательным trap в принятой модели. Другой цикл, который не проходит через проверяемую точку, не игнорируется: он даёт unknown.

Для максимальной длины последняя нормальная итерация имеет индекс 0xFFFFFFFE, после неё индекс становится 0xFFFFFFFF. Вычисление length + 1 не требуется. Это проверяется символически и отдельным граничным тестом.

Что именно доказывается

Обязательство	Содержание
Покрытие входных путей	Ни один допустимый вход не потерян
Инициализация	Каждый вход в цикл устанавливает инвариант; прямые выходы удовлетворяют контракту
Покрытие переходов	Все исходы одного обхода тела перечислены
Определённость	Нет `Undefined` на допустимом состоянии
Безопасность обращений Semantic IR	Нет bounds trap при корректном входном view
Точное условие trap	Trap происходит тогда и только тогда, когда следующий префикс суммы не представим
Сохранение инварианта	Каждый обратный переход устанавливает инвариант следующего состояния
Строгое уменьшение меры	Цикл не может продолжаться без прогресса
Переход префикса	Индекс увеличивается на один; аккумулятор соответствует следующему префиксу
Постусловие	Возврат соответствует первой позиции/отсутствию либо точной последовательной сумме

Для поиска trap не допускается. Для суммы точное условие проверяется при инварианте, который уже утверждает представимость всех предыдущих префиксов. Следовательно, до первого непредставимого префикса trap отсутствует, а при его вычислении неизбежен. Одной проверки «если вернулось, сумма правильная» здесь недостаточно.

Префикс S не строится перебором. Это математический объект, определённый суммированием. В SMT подставляются только истинные определяющие равенства S(0) = 0 и S(i+1) = S(i) + data[i] для текущего шага; прочие значения S не ограничиваются рекуррентными равенствами этого запроса. Это ослабляет предположения доказательства, не ограничивая входы. Настоящие математические префиксы удовлетворяют этим равенствам на каждом шаге.

Инвариант предполагается только при проверке произвольного перехода. Его установление на входе и сохранение на всех обратных рёбрах проверяются отдельно. Ложный инвариант не может пройти проверку входа.

Фактический Semantic IR и LLVM

Проверяются реальные блоки, операции и phi-узлы, произведённые компилятором. Роли индекса и аккумулятора задаются внешней схемой привязки к phi-узлам; идентификаторы и выбранная точка CFG сохраняются в отчёте. Правильность привязки не принимается как аксиома: входы, переходы, ранние выходы и результат обязаны пройти все проверки с этой привязкой.

LLVM проверяется независимо от доказательства Semantic IR. Сейчас поддержаны две фактические формы:

Заголовок с i32 phi и проверкой условия перед телом — generated/O0.
Заголовок тела с i64 индексом и проверкой выхода после итерации — O2.

Для второй формы инвариант усиливается до i < length: пустой вход обрабатывается до входа в тело. Его установление также доказывается, а не переносится механически с исходного цикла.

Внешний контракт view предполагает одно живое инициализированное readonly- размещение размером length × sizeof(element). Semantic IR использует символическую последовательность элементов; LLVM — отдельную байтовую модель с происхождением указателя, смещением, границами и выравниванием. Четыре байта i32 декодируются в little-endian. Неверный масштаб GEP обнаруживается отдельным негативным тестом.

Массивы SMT символические: объекты размером в миллиарды элементов физически не создаются. Значения байтов представлены математическими целыми с нормализацией modulo 256; это покрывает все байтовые последовательности.

Нет записи, освобождения, heap, внешних вызовов, aliasing или конкурентного изменения данных. Валидность входного view — условие теоремы, а не доказательство его создания или доступности такого объёма памяти на конкретной ОС.

Неподдерживаемые формы CFG, инструкции, атрибуты или результаты решателя помечаются unknown. Они не наследуют успех Semantic IR.

Результат первого набора

Представление	Обязательства для двух функций
Semantic IR	20
Сгенерированный LLVM IR	18
LLVM после O0	18
LLVM после O2	18
Всего	74

В LLVM безопасность физического доступа включена в отсутствие Undefined. В Semantic IR отсутствие bounds trap дополнительно выделено самостоятельным обязательством. Число запросов само по себе не измеряет глубину доказательства: ключевой результат здесь — индуктивная проверка и мера завершения.

Восемь отрицательных контролей

Поломка	Конкретное воспроизведение
`<= length` вместо `< length`	Пустой view вызывает bounds trap
Пропуск первого элемента	Поиск по `[7]` не находит `7`
Последнее совпадение вместо первого	Поиск по `[7, 7]` возвращает `1`
Индекс увеличивается на два	В `[0, 7]` пропускается искомый элемент
Индекс не увеличивается	Повторяется одно состояние; нарушается завершение
Убрана проверка переполнения	`[MAX, 1, -1]` возвращает `MAX` вместо trap
Слагаемые обходятся в обратном порядке	Тот же вход успешно завершается вместо trap на втором префиксе
Phi передаёт старый аккумулятор	Сумма `[1]` возвращает `0`

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

16 тестов проверяют сами правила индукции, недостаточный и ложный инварианты, меру завершения, максимальную длину, первый overflow/underflow, декодирование байтов, обе LLVM-формы, неподдерживаемый цикл и инструкции, неопределённость решателя, мутации и замороженные файлы V0/V1.

Воспроизведение и границы гарантии

В отдельном окружении с Z3 и Clang:

python -m pip install -r verification/requirements.txt
python -m unittest verification.v2.test_verifier -v
python verification/v2/check.py --output build/verified-v2

Доступны --clang и положительный --timeout-ms. CI запускает отдельные задания loops на Linux, macOS и Windows; артефакты — verified-v2-*. V0 и V1 продолжают работать своими независимыми заданиями.

Отчёт включает версии инструментов, точные хеши IR и моделей, выбранные точки CFG и phi-роли, поддерживаемые инструкции, предположения, SMT-запросы, контрпримеры к обязательствам и отдельные результаты конкретного прогона.

Доверенная база включает спецификации, реализацию правила индукции, интерпретаторы IR, модель памяти, генератор запросов, Z3 и среду исполнения. Они сами не верифицированы. Это не независимый сертификат доказательства и не доказательство корректности всего компилятора. Машинный backend, ABI, ОС, ownership и регионы остаются вне доказательства.

Семантика инструкций LLVM сверяется с LLVM Language Reference.