M0 — аудит контракта доступа

Этот аудит дополняет первые тесты и измерения M0. Он не меняет синтаксис, не оптимизирует JSON и не является универсальным доказательством borrow checker. Исходный предмет ревью — PR #22, HEAD 13ebb01.

Независимо заданные ожидания

tests/test_mutable_audit.py строит конечную матрицу по режимам параметров value, readonly, mutable и двум исходным объектам. Ожидаемая допустимость не читается из Semantic IR или журнала настоящего анализатора. Правила заданы отдельно: первый mutable-заём запрещает любой последующий доступ к тому же объекту; первый readonly-заём запрещает последующего писателя; обычное чтение значения создаёт независимый снимок до вычисления следующего аргумента.

• 36 комбинаций двух аргументов: 28 допустимы, 8 должны быть отвергнуты.
• 12 комбинаций с вложенным вызовом во втором аргументе: 8 допустимы, 4 отвергаются.
• Все допустимые комбинации первой матрицы исполняются нативно на O0/O2: проверяются результаты чтения, изменения обоих объектов и старые снимки.

Это конечный набор программ, а не перебор всех CFG, типов и lifetime-сценариев. И ожидаемые правила, и инструмент генерации тестов требуют ревью.

Наблюдаемый порядок

Нативный контроль записывает байт R из правой части присваивания в массив. При допустимом индексе байт появляется; при индексах 2 и 0xFFFFFFFF для массива длиной 2 программа должна завершиться trap без байта R. Используется настоящий console runtime, который пишет в канал процесса; результат проверяется отдельно от кода завершения. Это проверяет порядок bounds-check перед RHS I/O, а не только наличие какого-либо trap.

Другой контроль меняет поле, наблюдает его через readonly reborrow с I/O, затем возвращает Err. Вывод и состояние caller должны отражать уже выполненную запись. Автоматический rollback не подразумевается.

Найденный дефект и исправление

Предварительный поиск имён для mutable storage объединял одноимённые привязки из независимых лексических блоков. При наличии borrow mut value для структуры во втором блоке он мог ошибочно отвергнуть скалярную var value в первом. Это ложный отказ компилятора, а не обнаруженное нарушение исключительности.

В первом исправлении имена оставались консервативной подсказкой для размещения. Финальное ревью усилило это решение: и предварительный поиск адресуемых vars, и анализ конфликтов используют идентичности конкретных деклараций. Текстовое имя только разрешается в текущей лексической таблице; совпадение написания не объединяет ни права, ни storage.

У привязки отдельно хранятся тип, глубина области, идентификатор декларации, режим доступа и корни удерживаемых views. active_readers, active_writers и лексические loans содержат идентификаторы, а не имена. При присваивании личность привязки сохраняется; новая декларация в соседнем блоке получает другую. Идентификатор стабилен при повторном посещении AST в fixed-point анализе цикла. Он локален одному анализу и не сериализуется как адрес памяти или постоянный ID между компиляциями. В Semantic IR физические корни по-прежнему представлены отдельными SSA storage-значениями.

Регрессия проверяет скаляр → структура → скаляр с одним именем в трёх блоках. Дополнительно две одноимённые структуры не должны обе становиться адресуемыми, если заимствуется только одна; mutable-право не переносится на immutable-привязку в следующем блоке или другой ветви. Старый снимок изменяемой структуры остаётся независимым. Это не вводит shadowing или долгоживущие ссылки.

Свидетельства по требованиям

Требование	Проверка	Ограничение
Исключительность и readonly-конфликты	Матрица режимов, nested-call матрица, мутация отключения проверки	Только выбранные программы
Независимость снимков	Нативная матрица, small/large snapshots, мутация snapshot alias	Не универсальная теорема о storage lowering
Reborrow	Вложенные readonly/mutable вызовы и восстановление доступа после возврата	Только call-scoped займы целого объекта
Порядок аргументов	Разные порядки value/readonly/mutable и вложенные вызовы	Без двухфазного borrowing
Traps и порядок записи	Overflow-мутация, границы до RHS I/O, короткое замыкание	Не покрывает все преобразования LLVM
Прямые записи без copy-in/copy-out	LLVM-проверки small/large обновления поля, нативное наблюдение изменений	Явные снимки могут копироваться
JSON	6785 разбиений на O0 и O2, ожидаемые коды и смещения	Выбранный корпус, не доказательство всех входов
Платформы	Полный Compiler tests и нативные M0-контроли в Linux/macOS/Windows CI	Успех относится к конкретному HEAD

После исправления LLVM IR mutable JSON побайтово совпал с артефактом измеренного компилятора c5d5ec8: SHA-256 24290202046d9fe1029f94e26437c42e734d3b2f68111521538175a18c3ee8cd. Поэтому новый benchmark для этого исправления не выдаётся за новый результат производительности; сохраняется исходный отчёт и его границы.

M0 по-прежнему не включает ресурсные mutable borrows, заимствование поля как самостоятельного mutable-аргумента, возвращаемые/хранимые займы, потоки и shared memory. V0–V4, Relay и Alive2 не расширяют свои гарантии на весь M0 автоматически.