Справочник байткода и ВМ Лиспекса

Полный пример от исходника до результата приведён в руководстве по байткоду. Его файл refund-window.lpxbc содержит инструкции. JSON просмотра и сравнения описывает файл или запуск.

Прочитайте отчёт просмотра

Правило возврата из руководства даёт следующие поля отчёта bytecode inspect.

{
  "requirements": ["explicit-input"],
  "source_map_coverage": {
    "complete": true,
    "mapped_instructions": 22,
    "referenced_anchors": 11,
    "schema": "lispex.bytecode-source-map/v1",
    "total_anchors": 11,
    "total_instructions": 22
  }
}

Файл требует явного ввода. Все 22 инструкции связаны с позициями в исходнике и используют 11 разных якорей. Якорь задаёт строку и столбец исходного текста.

Полный отчёт также содержит идентификаторы исходника, Core IR и байткода, размеры таблиц, число инструкций по видам и позиции корней. Корень — выражение верхнего уровня. Отчёт указывает execution: "not-run" и authority: "integrity-only". После строгого декодирования, проверки и повторного кодирования bytecode validate возвращает valid: true.

Компиляция и идентификаторы

Native читает исходник, преобразует сокращения в формы Core и разрешает ссылки имён в lispex.core-ir/v1. Компилятор байткода превращает этот файл в lispex.bytecode/v1. Считыватель и проверяющий модуль проверяют байткод до выполнения в ВМ Лиспекса.

Так реализуется lispex-profile-1.5, включая синтаксис, виды данных, встроенные процедуры и поведение языка. Интерпретатор Лиспекса служит эталоном и по умолчанию выполняет исходники.

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

Идентификатор байткода использует следующий домен хеша.

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

Каноническое кодирование задаёт единственное байтовое представление всех записанных сведений, включая точный идентификатор исходника. У программ с одинаковым результатом могут различаться идентификаторы исходника и байткода.

Двоичное кодирование

Файл начинается с восьмибайтового префикса формата и версии, затем указывает фиксированное число секций. Известные теги секций должны строго возрастать. Перед содержимым каждой секции записана длина в байтах как u32 с порядком big-endian. Заполняющих и завершающих данных нет. Big-endian означает, что старший байт записан первым.

Порядок секций фиксирован.

identity
strings
constants
anchors
bindings
globals
scopes
functions
guards
blocks
roots

Индексы и размеры записаны как u32 с порядком big-endian. Текст — точный UTF-8 с предшествующей длиной в байтах. Для строк, констант, якорей, ID и ссылок заданы порядок и представление.

Считыватель проверяет пределы до выделения памяти и контролирует переполнение при вычислениях. Он проверяет UTF-8 и ожидаемые типы каждой таблицы. Затем повторно кодирует файл и требует побайтового совпадения.

Инструкции и проверка

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

До создания исполняемых констант, глобальных переменных, замыканий, входных привязок или состояния VM проверяются следующие элементы по порядку.

1. Префикс формата, секции, длины, каноническое кодирование и фиксированные идентификаторы.
2. Упорядоченные уникальные наборы общих данных, точная запись данных, непрерывные ID, роли таблиц и ссылки.
3. ID примитивов и глобальных переменных, лексическая видимость, перенаправляющие ячейки, захваты функций, описатели обработчиков и якоря исходника.
4. Достижимый поток управления, цели переходов, формы стека и результата, баланс областей, слияния ветвей, конечные хвостовые вызовы и полные возвраты.
5. Стоимость инструкций и суммарные ресурсные пределы.

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

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

Ресурсные пределы и диагностика

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

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

Выполнение в ВМ Лиспекса

VM явно хранит записи активного кода, лексических областей, возвратов, обработчиков исключений, guard и dynamic-wind. Она также поддерживает одноразовые продолжения. Хвостовой вызов заменяет запись активного кода без роста стека вызовов хоста. Замыкания совместно используют изменяемые ячейки, включая перенаправляющие ячейки динамических определений.

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

Дерево и VM входят в одно семейство продукта Rust. Их сравнение записывает результаты двух способов выполнения внутри этого семейства.

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

Ошибка выбранной VM возвращается от этого способа выполнения без запасного запуска. Справочник движков описывает текущее выполнение в Лиспексе и завершение поддержки LIL/LIT. Отчёты сравнения записываются по новым путям за один шаг.

Native предоставляет инструменты байткода и ВМ Лиспекса на поддерживаемых платформах. npm, открытый WASM и Песочница предоставляют выполнение исходника интерпретатором дерева и Изображения Лиспекса. Подробности платформ приведены в каталоге продуктов.

Скомпилированный байткод в Ваучере Лиспекса

Ваучер Лиспекса создаёт lispex.vouch-compiled-artifact/v1 из исходника, принимаемого профилем csk.checked-profile/v1. Сохраните этот полный исходник как vouch-rule.lspx, затем создайте и проверьте контейнер.

(if (exact-integer? input) (decision-approve) (decision-deny))

lispex vouch compiled build --source vouch-rule.lspx --out vouch-rule.lpxvca
lispex vouch compiled validate --artifact vouch-rule.lpxvca --source vouch-rule.lspx

Обе команды завершаются с кодом 0. Первая создаёт vouch-rule.lpxvca и печатает отчёт lispex.vouch-compiled-artifact-build/v1. Вторая печатает отчёт проверки со следующими полями.

{
  "compiled_artifact_validation": "lispex.vouch-compiled-artifact-validation/v1",
  "derivation": "exact-source",
  "execution": "not-run",
  "valid": true
}

Исходник правила возврата из руководства не соответствует csk.checked-profile/v1. Эта команда сборки отклоняет его с compiled-artifact-source-invalid и кодом 1. Для скомпилированного контейнера пишите исходник по правилам этого профиля.

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

Параметр --compiled-artifact команд vouch verify --reexecute и vouch gate выбирает этот контейнер. Native аутентифицирует и фиксирует запрос, повторно получает Core IR и байткод из исходника, проверяет текущее согласие дерева и Meaning. Затем он сравнивает запись выполнения проверенной ВМ Лиспекса. Отчёты просмотра, проверки, повторного выполнения и допуска описывают соответствующие шаги.

Компиляция для Ваучера использует артефакт ВМ Лиспекса, полученный из точного исходника потребителя.