Байткод, 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 и ссылки таблиц имеют единственный порядок и представление. Строгий reader проверяет пределы до выделения памяти, использует 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 и запрещённые fallback. Ограничение вывода покрывает точный порядок эффектов примитивов и автоматической печати верхнего уровня.

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

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

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

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

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

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

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

Точная граница Topaz VM

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

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

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

Статическая ветвь Topaz AOT

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

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

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

• lispex run --backend rust по умолчанию использует --engine tree.
• --engine vm выполняет в памяти source → Core IR → bytecode → verify → VM.
• Ошибка compile, verification, resource или runtime выбранного VM никогда не запускает tree как fallback.
• 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 выбирает точный установленный продукт Topaz.
• lispex compare-vms --topaz-vm ROOT --receipt FILE SOURCE один раз выводит байткод и записывает оси Rust/Topaz в lispex.topaz-vm-comparison/v1.

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

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

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

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

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

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

Обычный маршрут Topaz VM находится вне этой цепочки. Его запрос, результат, хэши, identity executable, вывод и отчёт сравнения не могут стать compiled artifact Vouch, наблюдением re-execution, handle evidence или grant gate.

Куда дальше

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

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