Liza Verified V4: Ownership & Region Dependencies

Эксперимент завершён в заявленных пределах.

V4 проверяет выбранный фрагмент Semantic IR: Region/Buffer, условное владение в Result, межпроцедурную передачу, phi и циклы. Независимая модель сравнивает исполнение с журналом настоящего анализатора Liza. Это проверка конкретных программ и опубликованных фактов, а не доказательство корректности всего анализатора для всех допустимых исходников.

Матрица включает 11 положительных программ, 7 мутаций анализатора и отдельные 8 контролей заниженных сводок возвращаемого происхождения. Все отрицательные контроли воспроизводятся с конкретной арифметикой. Удалённые платформенные результаты следует проверять по workflow V4; локальный результат сам по себе не подтверждает Linux/macOS/Windows CI. V0–V3 остаются отдельными неизменёнными наборами.

Два обязательства

Реальные живые зависимости должны входить в статическое приближение: D_real(s) ⊆ D_static(p).
При потенциально живом зависимом значении запрещены close и явный move региона.

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

Независимость модели

lower(..., dependency_audit=audit) по запросу сохраняет состояния настоящего анализатора до и после выражений. Включение журнала не меняет сериализованный Semantic IR. Журнал не участвует в решениях компилятора.

verification/v4/model.py восстанавливает ресурсы из операций IR. Модель не импортирует правила liza.dependencies, не использует storage_relation и не выбирает переходы по storage_contract. Журнал и сводки используются только для сравнения с независимо полученным состоянием.

Успешное создание региона выдаёт свежую логическую идентичность; буфер ссылается на конкретный экземпляр. move потребляет доступное значение, release снимает зависимость, close проверяет живые буферы. Условный ресурс внутри неразобранного Result сохраняется. Выбор match определяется фактическим тегом, а не сводкой анализатора.

Журнал содержит контрольные точки выражений, а не отдельное состояние перед каждой синтетической инструкцией. variant.tag, variant.payload и phi выполняются по независимым правилам модели; последующие наблюдения сравниваются с состоянием соответствующего пути. Соответствие AST/SSA остаётся явным предположением, а не доказанным свойством компилятора.

V4-B: функции и сводки

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

На каждом нормальном возврате отдельно проверяются:

происхождение возвращаемого ресурса против storage_contract.returns;
отсутствие оставшихся непереданных обязанностей функции.

Правильный origin возвращённого буфера не оправдывает потерю второго буфера. Объявление normal_exit не принимается за доказательство: модель сама проверяет незавершённые обязанности. Избыточная сводка допустима как консервативное приближение; недостаточная даёт summary_failure.

Матрица включает generic-передачу буфера и Result, конструирование Ok, обновление буфера, фабрику региона, два буфера одного региона и два различных региона. Проверяются только функции и состояния, достижимые из выбранного main; это не универсальная теорема о каждой функции при любых параметрах.

Что именно означает «сводка проверена»

V4 не сертифицирует весь словарь storage_contract. Область проверки явно записывается в summary_scope каждого отчёта:

Часть контракта	Обязательство V4
`returns.regions` / `returns.depends_on`	Покрыть реальное происхождение возвращённого ресурса
`returns.variants`	Покрыть ресурс именно в выбранном варианте, включая `Ok`
Нормальный выход	Исполнение тела не оставляет непереданных обязанностей
Аннотация `normal_exit`	Не аксиома; её текст не подтверждает завершение владения
`requires`, `consumes`, `effects`, `parameters`, `creation_sites`, `returned_buffer_storage`, `trap_cleanup`	Полнота этих полей как опубликованных сводок отдельно не сертифицируется

Спорный тест с заменой сводки на {'deliberately': 'false'} относится только к main() -> u32, которая не возвращает ресурс. Здесь обязательство возвращаемого происхождения пусто; остаётся операционная проверка завершения владения. verified_fragment в этом тесте не означает, что произвольный словарь является корректной полной сводкой. Тест назван соответственно.

Отдельная матрица меняет только storage_contract, оставляя тело Semantic IR и журнал анализатора неизменными:

Контроль	Скрываемое свойство
Пустой `depends_on` прямого результата	Зависимость generic-возврата буфера
Отсутствующий ключ `returns`	Всё возвращаемое происхождение
Удалённый `Ok`	Условно принадлежащий буфер после generic-передачи `Result`
Пустой `depends_on` сконструированного `Ok`	Зависимость буфера внутри результата
Перенос описания `Ok` в `Err`	Соответствие зависимости фактическому варианту
Подмена параметра происхождения	Принадлежность одному из двух различных регионов
Пустой `regions` фабрики	Владение возвращаемым новым регионом
Подмена пути параметра `Ok` на `Err`	Происхождение payload входного `Result`

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

Отдельные положительные контроли сохраняют консервативность: лишнее происхождение допустимо; параметры двух буферов одного региона могут обозначать одну реальную зависимость. Поэтому тест неверного параметра использует именно два различных региона.

summary_failure сообщает нарушение проверяемого утверждения о возврате, а не автоматически уязвимость освобождения памяти. Для остальных программ абстрактное расхождение сводки не обещает конкретной достижимости. В этой отдельной матрице она проверяется дополнительным конкретным проходом. Прежнее правило остаётся: невоспроизводимый абстрактный путь опасной операции даёт unknown; model_violation требует подтверждённой трассы.

V4-C: CFG и phi

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

Скалярная арифметика и сравнения в абстрактном проходе дают неизвестное скалярное значение. Неизвестное условие исследуется в обе стороны. Это консервативное приближение числового управления, а не попытка заново доказать арифметику V0–V2. Дополнительные пути могут давать недостижимые контрпримеры; их нельзя автоматически объявлять ошибками программы.

V4-D: циклы и индуктивное замыкание

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

При сравнении состояний идентификаторы живых ресурсов переименовываются взаимно однозначно. Два одновременно живых экземпляра одной точки создания остаются различными. Завершённые экземпляры не требуют бесконечного накопления истории. Счётчик свежих идентификаторов не используется как статический origin и не мешает замыканию ресурсно нейтрального цикла.

Если все преемники достижимого состояния проверены и возвращаются в уже исследованный граф, множество состояний замкнуто относительно переходов. Оно служит индуктивным инвариантом безопасности: начальное состояние входит в него, каждый поддержанный переход сохраняет принадлежность, запрещённые операции отсутствуют. Это не разворачивание заданного числа итераций. Тест замены границы цикла 2 на 4294967295 сохраняет число исследованных состояний. Завершение цикла не доказывается; ресурсно безопасный бесконечный цикл не обязан иметь нормальный выход.

Поддержанные примеры сохраняют origins внешних владельцев на обратном ребре или завершают локальные ресурсы до следующей итерации. Если граф растёт и бюджет исчерпан, результат — unknown, а не успех на проверенном префиксе. Хеши исследованных абстрактных состояний и число замыкающих переходов входят в отчёт. Это диагностические артефакты доверенной модели, не сертификат для отдельного малого формального ядра.

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

Мутация	Наблюдаемое нарушение
Потеря зависимости payload `Ok`	Перемещение региона при живом буфере
Потеря зависимости неразобранного `Result`	Преждевременное перемещение региона
Неверная подстановка origin результата вызова	Буфер остаётся зависимым от исходного региона
Потеря зависимости при объединении ветвей	`phi` передаёт живой буфер на опасный путь
Отключение guard региона	Зависимость опубликована, операция разрешена
Подмена одного региона другим	Закрывается регион, реально содержащий буфер
Отключение сохранения origins на обратном ребре	Второй проход закрывает регион с буфером предыдущего прохода

Для каждого случая неизменённый компилятор отвергает исходник. Обвязка загружает в память изменённый анализатор и компилирует тот же исходник остальными обычными проходами. Затем проверяются принятый IR и журнал. Файл анализатора в репозитории не изменяется.

Каждая трасса нарушения повторяется с конкретными скалярными вычислениями, checked-арифметикой и проверкой границ buffer.update. Последовательность исходов выделения фиксируется из абстрактного пути. Ветвь, противоречащая конкретному условию, не считается воспроизведённой. Отдельные тесты проверяют невозможную ветвь 1 == 2 и обязательный bounds trap до опасной операции.

Replay использует те же правила ресурсов, но иной режим скалярных переходов. Он подтверждает путь в модели, а не независимо доказывает корректность самой модели. Реальный allocator и native-бинарник не исполняются. Ok/Err выделения — абстрактные исходы; вместимость, выравнивание и реальные отказы ОС остаются вне эксперимента.

Статусы и границы

Статус	Значение
`verified_fragment`	Достижимый граф замкнут, поддержанные переходы безопасны, опубликованные факты покрывают зависимости
`coverage_failure`	Недостаточное статическое покрытие; без воспроизведённой опасной операции это ещё не установленная уязвимость
`guard_failure`	Принята операция, запрещённая опубликованным приближением
`summary_failure`	Возвращаемое происхождение не покрыто сводкой функции
`model_violation`	Конкретный повторный проход воспроизвёл запрещённую операцию или потерю обязанности
`unknown`	Неподдержанный переход, недостающие наблюдения, бюджет или невоспроизводимый абстрактный контрпример

Поддержаны constant, операции создания/выделения/закрытия региона, buffer.release, buffer.update, buffer.length, move, скалярный copy, операции вариантов, пользовательские call, phi, целочисленные add/sub/mul, сравнения и терминаторы jump/branch/switch/return. Абстрактное продолжение после потенциально падающей арифметики или обновления является приближением нормальных путей; точные traps проверяются только при replay поддержанных операций. Проверка V4 не заменяет V0–V2.

Пока не поддержаны рекурсивные вызовы, пользовательские borrowed-параметры, readonly views, линейные произведения, Vec, файловые ресурсы и произвольные инструкции IR. Не проверяются allocator, LLVM, машинный код и конкурентность. Неиспользованные коды ошибок выделения абстрагируются; неподдержанная операция над ними не получает доказанного результата.

Доверенная база: интерпретатор ресурсов, скалярная абстракция и replay, алгоритм замыкания и переименования, соответствие AST/SSA, декларации типов, сериализация и Python. Собственные сводки анализатора в неё как аксиомы не входят. Для выбранного фрагмента проверяется отсутствие преждевременного освобождения; общей формальной гарантии для всех программ Liza это не даёт.

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

python3 -m unittest verification.v4.test_model -v
python3 -m verification.v4.check --output build/verified-v4

Отчёт содержит проверенные функции, статусы, факты покрытия и guard, ошибки сводок, трассы с результатами replay, исходные отказы компилятора, хеши IR и журнала, версии Python/платформы и SHA-256 инструмента и мутантов. Workflow запускает эту матрицу отдельно на Linux/macOS/Windows. Успешный exit обвязки требует подтверждения всех положительных программ и воспроизведения всех семи мутаций анализатора, а также отказа на восьми заниженных сводках в обоих режимах. unknown не проходит.