Liza Verified V1: Bounds and Control Flow

Отдельное расширение Verified V0, без изменения языка 0.0.25. V1 проверяет восемь фиксированных функций на фактическом Semantic IR, сгенерированном LLVM IR и LLVM IR после O0/O2: 32 обязательства.

Все четыре элемента [u8; 4] символические, как и заменяющее значение. Индекс имеет полный диапазон u32: от 0 до 0xFFFFFFFF. Предположения index < 4 на входе нет: выход за границы обязан давать trap.

Контракты функций

Функция	Что проверяется
`read`	Чтение нужного элемента либо обязательный bounds trap
`update`	Замена выбранного элемента; остальные элементы сохраняются
`snapshot`	Обновление копии не изменяет исходное логическое значение
`short_and`	Правая часть `&&` вычисляется только при истинной левой
`short_or`	Правая часть `\|\|` вычисляется только при ложной левой
`branch`	Неисполняемая ветвь не вызывает trap
`constant_read`	Чтение элемента после устранения физического размещения
`choose`	Объединение значений через phi или `select`

Для наблюдения за обновлением используется отдельный параметр observe: u32. Выражение observe & 3 покрывает все четыре позиции массива. Индекс обновления не маскируется и не сужается.

snapshot возвращает два наблюдения, упакованные в u16: исходный элемент в младших восьми битах, обновлённый — в старших. Поскольку проверяются все значения observe, доказательство охватывает сохранение каждого исходного элемента и корректность каждого обновлённого. Это позволяет проверять два логических значения, не добавляя ABI возврата агрегатов в область эксперимента.

fn read(a:u8,b:u8,c:u8,d:u8,index:u32)->u8 {
 data:[u8;4]=[a,b,c,d]
 return data[index]
}
fn update(a:u8,b:u8,c:u8,d:u8,index:u32,value:u8,observe:u32)->u8 {
 var data:[u8;4]=[a,b,c,d]
 data[index]=value
 return data[observe & 3]
}
fn snapshot(a:u8,b:u8,c:u8,d:u8,index:u32,value:u8,observe:u32)->u16 {
 original:[u8;4]=[a,b,c,d]
 var updated=copy original
 updated[index]=value
 j=observe & 3
 return u16(original[j]) | (u16(updated[j]) << 8)
}
fn short_and(a:u8,b:u8,c:u8,d:u8,index:u32,take:bool)->bool {
 data:[u8;4]=[a,b,c,d]
 return take && data[index]==a
}
fn short_or(a:u8,b:u8,c:u8,d:u8,index:u32,take:bool)->bool {
 data:[u8;4]=[a,b,c,d]
 return take || data[index]==a
}
fn branch(a:u8,b:u8,c:u8,d:u8,index:u32,take:bool)->u8 {
 data:[u8;4]=[a,b,c,d]
 if take {return data[index]}
 return a
}
fn constant_read(a:u8,b:u8,c:u8,d:u8,index:u32)->u8 {
 data:[u8;4]=[a,b,c,d]
 return data[2]
}
fn choose(a:u8,b:u8,c:u8,d:u8,index:u32,take:bool)->u8 {
 var result=a
 if take {result=b}
 return result
}
fn main()->u32{return 0}

Две разные модели

Semantic IR: массив — неизменяемый кортеж четырёх значений. array.update создаёт новый кортеж. У этой модели нет адресов, размещений или физических алиасов. Проверки границ явно создают исход trap.

LLVM IR: память состоит из различных локальных объектов размещения. Указатель содержит происхождение объекта и символическое смещение в байтах. Для каждого байта отдельно хранятся содержимое и признак инициализации. store изменяет байты объекта, а load проверяет границы, выравнивание и инициализацию всех читаемых байтов.

Поэтому правильное условие index < 4 ещё не обеспечивает успех проверки: загрузка по неправильному смещению или запись в память исходного снимка обнаруживаются независимо от bounds condition.

После O2 память не обязательна. Поддерживаются и операции над значениями: insertvalue, extractvalue, phi, select, а также ограниченные операции над четырёхбайтовыми векторами. На проверенном lowering обновлений O2 использует векторные загрузки/записи; constant_read обходится без памяти.

Исходы исполнения и результат проверки

Модель программы различает:

Исход	Смысл
`Return(value)`	Возвращено определённое значение
`Trap`	Выполнен обязательный `llvm.trap`
`Undefined`	Нарушена модель LLVM: недопустимый доступ, неинициализированное чтение, poison и т. п.

Спецификация Liza допускает только первые два исхода. Undefined никогда не считается реализацией обязательного trap, даже если оба приводили бы к аварии на некоторой машине.

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

При контрпримере отчёт содержит входы, повторный расчёт спецификации обычными целыми Python и исход модели IR с причиной нарушения памяти.

Ограничения физической модели

Little-endian, 64-битное адресное/индексное пространство.
Успешные различные локальные размещения размером 1–16 байтов; исчерпание стека не моделируется.
Объекты живы до конца функции. Нет heap, внешних указателей, глобальных объектов, освобождения, lifetime intrinsics и преобразования чисел в адреса.
Читаются только инициализированные байты внутри своего объекта.
Выравнивание берётся из alloca. Требование доступа сильнее известного выравнивания размещения даёт unknown.
Арифметическое оборачивание смещений исключено консервативно. inbounds проверяет также промежуточные смещения; указатель на байт сразу за объектом можно сформировать, но нельзя разыменовать.
nuw для GEP поддерживается вместе с inbounds; отрицательные смещения с nuw консервативно отвергаются.
Достижимое создание poison и чтение неинициализированного байта считаются Undefined, даже если результат затем не используется. Это более строгая модель, чем полная семантика LLVM с undef/poison.
Циклы, неизвестные инструкции, метаданные и неподдерживаемые атрибуты дают unknown. Пользовательские вызовы не поддерживаются.

Атрибуты nneg, nuw, nsw, disjoint и returned в поддерживаемом фрагменте проверяются как обязательства, а не принимаются на доверии. Точный список поддерживаемых инструкций и предположений сохраняется в отчёте.

V1 сравнивает результаты и обязательные traps. Он не доказывает произвольный порядок эффектов: если перестановка двух вычислений не меняет наблюдаемый исход в этой модели, отличить её нельзя. В выбранных примерах проверяется именно отсутствие вычисления опасной невыбранной ветви или правого операнда.

Девять намеренных поломок

Мутация	Обнаруживаемое нарушение
`< 4` заменено на `<= 4`	Индекс `4` допускается к чтению за объектом
Знаковое сравнение вместо беззнакового	Большой `u32` ошибочно проходит проверку
Усечение индекса перед проверкой	Недопустимый индекс превращается в допустимый
Смещение загрузки на один байт	Читается соседний элемент либо байт вне объекта
Дополнительная запись в соседний элемент	Изменяется элемент, который должен сохраниться
Scratch обновления совмещён с исходным снимком	Старое наблюдаемое значение меняется
Принудительное вычисление RHS `&&`	Возникает trap при ложном левом операнде
Принудительное вычисление RHS `\|\|`	Возникает trap при истинном левом операнде
Загрузка из неинициализированного объекта	`Undefined` даже при допустимом адресе

Мутации применяются к реальному сгенерированному LLVM IR. Они сохраняются как полные модули и проходят синтаксическую проверку Clang; для отрицательных контролей проверяется исходный мутированный IR, не его оптимизированная версия. Все девять мутаций должны дать counterexample, а не unknown.

24 теста самого инструмента дополнительно проверяют символическую инициализацию, разные происхождения и реальные алиасы, разделение памяти между путями CFG, выравнивание, byte order, 0xFFFFFFFF, атрибуты оптимизатора, SSA без памяти, неопределённость решателя и неизменность исходников V0. Они не являются доказательством корректности модели.

Воспроизведение и артефакты

Используется то же отдельное окружение с Z3, что и для V0:

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

Clang должен быть в PATH; доступны --clang и --timeout-ms. V0 продолжает запускаться своей командой python verification/check.py и сохраняет отдельные результаты. Его файлы привязаны к замороженному SHA-256-манифесту; V1 не меняет их содержимое.

Каждое обязательство V1 указывает файл проверенного IR и SHA-256 его точных байтов. Отчёт также содержит запросы SMT-LIB, хеши моделей, версии Z3/Clang, предположения, встреченные инструкции, контрпримеры и манифест V0. Хеш относится ко всему модулю, а область утверждения — к указанной функции.

Отдельные задания bounds в CI запускаются на Linux, macOS и Windows; артефакты называются verified-v1-*. Задания V0 arithmetic сохранены отдельно.

Это проверка соответствия выбранных IR в доверенной модели с Z3. Ни SMT-LIB запросы, ни хеши не являются независимыми сертификатами доказательства. Модель и генератор обязательств сами не верифицированы. Машинный код, ABI, ОС, ownership, регионы и общая безопасность памяти остаются вне доказательства.

Источник семантики поддерживаемых инструкций: LLVM Language Reference.