Байткод, 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, примитивы и семантику. 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. стоимость инструкций и суммарные ресурсные пределы

Verifier отклоняет неизвестный opcode, оборванную ссылку, неканоническую константу, несовместимое слияние, остаток stack, несбалансированный scope, отсутствующий return и недостижимую инструкцию. Успешная проверка записывает структурную допустимость. Ваучер добавляет происхождение и политику доверия.

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

• размер артефакта до 32 MiB
• до 100 000 записей в каждом основном pool или table
• до 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 и счётчиков запасных путей. Закрытый выбор продукта сохраняет ошибки на выбранном маршруте Топаза.

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

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

Это полно-профильный маршрут корректности с явным соглашением о вызовах и записью всех идентификаторов компиляции. Используйте 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.
• LIL и LIT выбираются через свои семейства бэкендов.
• 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.

Отчёт публикуется атомарно и служит диагностическим материалом для просмотра и сравнения. Ваучер использует отдельный связанный с исходником compiled artifact.

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

Неподдерживаемые ячейки возвращают явный статус и сохраняют выбранный движок.

Как проверенный байткод входит в Ваучер

Ваучер выводит скомпилированное свидетельство из точного исходника или канонического изображения Лиспекса, которое его восстанавливает. Аутентификация производителя, политика получателя, ввод потребителя, согласие движков и шлюз решения сохраняют отдельные явные записи.

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

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

Куда дальше

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

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