Байткод, verifier и Native VM

Конвейер продукта

точный исходник
  -> reader и гигиенический normalizer
  -> lispex.core-ir/v1
  -> детерминированный compiler байткода
  -> lispex.bytecode/v1
  -> строгий reader и verifier
  -> lispex-rust-vm/v1
  -> обычные outcome, вывод, предупреждения и диагностика Лиспекса

Конвейер компилирует существующий lispex-profile-1.5. Он не добавляет синтаксис, datum, примитивы, неявный I/O или новый семантический профиль. Tree-интерпретатор остаётся эталоном и стандартным движком Rust.

Фиксированные идентификаторы

Заголовок связывает точную идентичность исходника, хэш Core IR, tag и хэш реестра примитивов, профиль, идентификаторы инструкций/source map/стоимости, производителя и сортированные требования. Инструмент сообщает версию продукта, но она не меняет стабильные семантические байты.

Идентичность артефакта вычисляется так.

SHA-256("lispex/bytecode-hash/v1" || 0x00 || canonical-bytecode-bytes)

Производитель сообщает происхождение, а не доверие.

Канонический бинарный envelope

Бинарный формат содержит один восьмибайтовый prefix magic/version, фиксированное число секций, строго возрастающие известные tags, длину каждого payload как big-endian u32 и никаких padding или trailer.

Допустим только один порядок, показанный ниже.

identity
strings
constants
anchors
bindings
globals
scopes
functions
guards
blocks
roots

Индексы и размеры записаны как big-endian u32. Текст записан как точный UTF-8 с длиной в байтах. Строки, константы, координаты, ID и ссылки таблиц имеют единственный порядок и представление. Строгий считыватель проверяет пределы до выделения памяти, использует checked arithmetic, проверяет UTF-8 и типизированные таблицы, затем повторно кодирует и требует побайтового совпадения.

Семейства инструкций

Блоки состоят из линейных инструкций. Переходы указывают на индексы декодированных инструкций, а не на смещения байтов. Порядок исходника сохраняется. Compiler не выполняет constant folding, удаление мёртвого кода, перестановку, inlining, числовую перегруппировку или новое определение хвостовой позиции. Он копирует разрешённый контракт Core IR.

Порядок проверки

До появления констант, globals, замыканий, ввода или состояния VM verifier проверяет по порядку перечисленное ниже.

1. magic, секции, длины, каноническое кодирование и фиксированные identity
2. сортированные уникальные pools, точное представление datum, непрерывные ID, роли таблиц и все ссылки
3. identity примитивов и globals, лексическую видимость, forwarding overlays, захваты функций, guard descriptors и координаты исходника
4. достижимый control flow, цели переходов, формы stack и outcome, баланс scope, слияния ветвей, терминальные tail calls и полные returns
5. стоимость инструкций и суммарные ресурсные пределы

Неизвестный opcode, оборванная ссылка, неканоническая константа, несовместимое слияние, остаток stack, несбалансированный scope, отсутствующий return или недостижимая инструкция отклоняются fail-closed. Проверка устанавливает структурную допустимость, а не эквивалентность смысла или доверие производителю.

Пределы и модель ресурсов

• размер артефакта не более 32 MiB
• каждый основной pool или table не более 100 000 записей
• каждый список операндов переменной длины не более 100 000 записей
• статическая проверка, то есть ограниченная линейная работа по инструкциям и рёбрам

Каждая выполненная инструкция, dispatch примитива и переход к гостевой процедуре имеют версионированную неотрицательную стоимость. Результат сообщает выбранные пределы, число переходов, байты вывода, максимум явных control frames, завершённые roots и число запрещённых запасных путей. Ограничение вывода покрывает точный порядок эффектов примитивов и автоматической печати верхнего уровня.

Исчерпание ресурсов остаётся ошибкой движка, а не перехватываемым условием Лиспекса. Глубина рекурсии tree и переходы VM принадлежат разным ресурсным профилям, и одинаковая семантика не означает одинаковых числовых пределов.

Source map и диагностика

Каждая инструкция ссылается на положительные строку и столбец из Core IR. Путь, имя хоста, время и выбор перевода строки не сохраняются. Ошибка исполнения использует координату текущей инструкции, поэтому сравнение tree/VM проверяет код, позицию, сообщение, частичный вывод и предупреждения как семантические оси.

Модель исполнения Rust VM

VM явно управляет code activations, lexical scopes, return frames, handlers, состоянием guard и wind, а также одноразовыми продолжениями. Хвостовой вызов заменяет текущую активацию и не увеличивает host stack. Замыкания сохраняют общие изменяемые ячейки, включая forwarding overlays динамических define.

Доступны все 205 строк текущего реестра примитивов. Обычные листья разделяют установленный Rust-код значений, чисел, aggregates, rendering, диагностики и writer. Восемнадцать примитивов, вызывающих гостевые процедуры, используют собственные итеративные машины VM, среди которых mapping, folds, apply, call-with-values, обработчики исключений, продолжения и dynamic-wind. Они не входят в tree-интерпретатор.

Структура VM отличается от tree, но это та же линия продукта Rust. Это маршрут дифференциального выполнения, а не четвёртое независимое семейство бэкенда.

Точная граница VM Топаза

Необязательный маршрут Топаза читает те же канонические байты отдельными считывателем, verifier и VM с явным управлением, написанными на Топазе. Он доступен только в Native macOS ARM64 с точным отдельно установленным продуктом Топаза 5.11.

До запуска Лиспекс проверяет manifest провайдера, артефакт Топаза, executable, wrapper, управляемые файлы, линию исходника/compiler, target, registry примитивов и пять нулевых счётчиков запасных путей. Закрытый запрос связывает точные исходник, Core IR, байткод, необязательный канонический ввод, полный предел u64, структурные пределы и идентичности продукта. Private staging имеет режим 0700, дочерний процесс получает очищенную среду с фиксированными системным PATH и локалью C, а процесс, его вывод и JSON результата ограничены, включая timeout.

Результат недоверен до проверки хэша запроса, invocation, идентичностей, канонического десятичного u64, пары status/exit, учёта вывода, структурных счётчиков, target, lineage и счётчиков запасных путей. Ошибка остаётся ошибкой Топаза, потому что нет поиска через PATH, репозиторий или сеть и нет повтора в Rust/tree/LIL/LIT либо старой версии Топаза.

Статическая ветвь AOT Топаза

AOT означает компиляцию заранее, когда правило превращается в отдельную программу до запуска и во время работы ничего не компилируется. Native macOS ARM64 может вывести проверенный граф управления в читаемый Топаз и собрать executable без исходника точным установленным компилятором Топаза 5.11 и точными Rust tool proxy. Установленный продукт связывает исходник, Core IR, байткод, пакет сгенерированного исходника, source map, topaz.artifact.v1, executable, producer, target, запрос ресурсов и пять нулевых счётчиков запасных путей. Во время запуска байткод не читается и другой движок не вызывается.

Это полно-профильный маршрут корректности, а не оптимизированное соглашение о вызовах и не доказательство сохранения смысла компилятором. Используйте lispex aot build|inspect|validate|run, а точный процесс описан на странице Сборка заранее скомпилированного продукта.

Выбор и сравнение движков

• lispex run --backend rust по умолчанию использует --engine tree.
• --engine vm выполняет в памяти source → Core IR → bytecode → verify → VM.
• Ошибка compile, verification, resource или runtime выбранного VM никогда не запускает tree как запасной путь.
• LIL и LIT остаются семействами бэкендов, и --engine их не переключает.
• lispex compare-engines --receipt FILE SOURCE пишет точные промежуточные identity и оси семантического расхождения в lispex.rust-engine-comparison/v1.
• lispex bytecode run --engine topaz --topaz-vm ROOT --bytecode FILE выбирает точный установленный продукт Топаза.
• lispex compare-vms --topaz-vm ROOT --receipt FILE SOURCE один раз выводит байткод и записывает оси Rust/Топаза в lispex.topaz-vm-comparison/v1.

Отчёт не перезаписывается, служит диагностикой и не может стать исполняемым артефактом или полномочием.

Поддержка продуктов

Неподдерживаемые продукты не имитируют бинарный формат в JavaScript и не переключаются молча на другой движок.

Целостность входит в Ваучер только через точное выведение

Каноничность и проверка байткода не доказывают, что компилятор сохранил смысл. Они не аутентифицируют производителя, не одобряют правило, не выбирают ввод потребителя, не устанавливают текущее согласие семейств и не дают решение. Корнем полномочий Ваучера остаётся точный исходник либо полностью доказанное изображение, которое его восстанавливает. Обычные байты и хэши байткода, отчёты inspection и validation, результаты VM и сравнения tree/VM входами Ваучера не являются.

Native может явно построить из точного исходника lispex.vouch-compiled-artifact/v1. Скомпилированный вызов Ваучера сначала аутентифицирует и закрепляет запрос, заново выводит Core IR и байткод, сохраняет согласие текущего tree/Meaning и лишь затем сравнивает протокол проверенной Rust VM. Контейнер не заменяет исходник или вход, а его отчёты inspection, validation, повторного выполнения и проверки допуска не создают живое свидетельство.

Обычный маршрут VM Топаза находится вне этой цепочки. Его запрос, результат, хэши, идентичность исполняемого файла, вывод и отчёт сравнения не могут стать скомпилированным артефактом Ваучера, наблюдением повторного выполнения, живым свидетельством или разрешением проверки допуска.

Куда дальше

Команды и восстановление разобраны в руководстве, а разрешённый входной контракт описан в справочнике Core IR.

Запуск проверенного байткода · Контракт Core IR · Проверенные поверхности