Песочница

Запуск проверенного байткода

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

Подготовьте правило и ввод

Сохраните refund-window.lspx.

LISPEX
(define (decide days)
  (if (<= days 30) 'refund 'review))

(decide input)

Единственный входной datum сохраните как request.lspx.

LISPEX
14

input не читает файл или окружение. Это явное требование, записанное в Core IR и байткоде, а значение передаётся отдельным параметром команды.

Соберите Core IR и байткод

SH
lispex core-ir build \
  --source refund-window.lspx \
  --out refund-window.lpxir

lispex bytecode build \
  --ir refund-window.lpxir \
  --out refund-window.lpxbc

Первая команда разрешает имена и ячейки, захваты, хвостовые позиции и координаты исходника, не выполняя правило. Вторая переводит этот Core IR в lispex.bytecode/v1, проверяет результат и записывает новый бинарный артефакт. Существующий файл ни одна команда не перезаписывает.

Изучите или проверьте до запуска

SH
lispex bytecode inspect --bytecode refund-window.lpxbc
lispex bytecode validate --bytecode refund-window.lpxbc

inspect показывает идентификаторы, размеры таблиц в заданных пределах, требования, число opcode, координаты корней и покрытие карты исходника. validate является более краткой границей для автоматизации. Строгий разборщик проверяет и заново кодирует артефакт, принимая только одно допустимое представление байтов.

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

Выполните только после проверки

SH
lispex bytecode run \
  --bytecode refund-window.lpxbc \
  --input request.lspx

OUTPUT

refund

Native CLI проверяет весь артефакт до создания состояния виртуальной машины. Некорректные байты отклоняются до чтения ввода, вывода, вызова примитива или первого шага машины. Если артефакт объявляет input, параметр --input обязателен, а лишний ввод для артефакта без такого требования также отклоняется.

Один stdin нельзя использовать сразу для двух входов, и такой вызов отклоняется.

SH
lispex bytecode run --bytecode - --input -

Передайте байткод или datum через именованный файл.

Выполните тот же артефакт в виртуальной машине Топаза

Виртуальная машина Rust встроена и остаётся вариантом по умолчанию. На macOS ARM64 можно явно выбрать точный допущенный продукт Топаза 5.11.

SH
lispex bytecode run \
  --engine topaz \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --bytecode refund-window.lpxbc \
  --input request.lspx

Корень продукта задаётся абсолютным путём к отдельно установленному lispex-topaz-vm/v1. Лиспекс проверяет манифест, артефакт Топаза, исполняемый файл, обёртку, управляемые файлы, линию компилятора и исходника, платформу, ресурсный контракт и объявление об отсутствии запасного пути. Поиска через PATH, соседний репозиторий, сеть или старую установку нет. Отсутствующий, изменённый, зависший или некорректный продукт даёт явную ошибку Топаза без повтора в Rust.

Выберите виртуальную машину для исходника

Для самодостаточного исходника есть короткая форма.

SH
lispex run --backend rust --engine vm rule.lspx

По умолчанию остаётся tree.

SH
lispex run --backend rust --engine tree rule.lspx

Явно выбранный vm никогда не повторяет неудачный запуск через tree. --engine относится только к Rust-бэкенду. Сочетание с другим бэкендом, таким как LIL или LIT, или с реестром внешних бэкендов является ошибкой использования.

Сравните два Rust-движка

SH
lispex compare-engines \
  --receipt tree-vm.json \
  rule.lspx

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

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

SH
lispex compare-vms \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --receipt rust-topaz.json \
  rule.lspx

Байткод выводится один раз, затем Rust и Топаз запускаются явно. Сравниваются статус, вывод, значения, предупреждения, диагностика, ресурсы и завершённые корни. Исходник Топаза структурно отделён, но исполняемый файл создан Rust Stage 0 компилятора Топаза. Отчёт записывает поддерживаемый исходник Топаза и идентичность producer Топаз Rust Stage 0 как дифференциальное свидетельство маршрута.

Когда собран соответствующий заранее скомпилированный продукт, сравните все четыре способа выполнения в Native.

SH
lispex compare-routes \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --aot-product /absolute/path/to/refund-window-aot \
  --receipt four-routes.json \
  --input request.lspx \
  refund-window.lspx

Команда использует один результат первого этапа и один проверенный байткод для запуска tree, виртуальной машины Rust, виртуальной машины Топаза и заранее скомпилированного продукта. Несовпадение исходника, Core IR или байткода отклоняет скомпилированный продукт до запуска. Квитанция не перезаписывает файл, отдельно записывает семантические и сопоставимые ресурсные оси, показывает линии и счётчик запасных путей. Ваучер использует связанный с исходником compiled artifact, описанный ниже.

Выберите подходящий продукт

ПродуктРоль исполнения
Native CLI на macOS ARM64инструменты байткода, встроенная виртуальная машина Rust, точная виртуальная машина Топаза, заранее скомпилированный продукт и сравнение четырёх способов
Native на других поддерживаемых платформахинструменты байткода и встроенная виртуальная машина Rust
npm CLI и пакетtree-выполнение исходника и точные Образы Лиспекса
Открытая сборка WebAssemblytree-выполнение исходника и точные Образы Лиспекса
Песочницаинтерактивное tree-выполнение исходника и точные Образы Лиспекса

Native владеет чтением, проверкой и виртуальной машиной байткода. Остальные продукты владеют своими потоками исходника и точных Образов Лиспекса.

Добавьте проверенный байткод в Ваучер

Хэш байткода идентифицирует точные байты, проверка фиксирует структурную допустимость, а локальный запуск виртуальной машины создаёт наблюдение Native. Ваучер добавляет аутентификацию издателя, политику доверия, точные исходник и ввод, текущее согласие tree и Meaning и решение локальной проверки допуска через контейнер, связанный с исходником.

Если потребитель намеренно добавляет согласие виртуальной машины к существующим проверкам Ваучера, Native создаёт отдельный контейнер, связанный с исходником.

SH
lispex vouch compiled build \
  --source refund-window.lspx \
  --out refund-window.lpxvca

lispex vouch compiled validate \
  --artifact refund-window.lpxvca \
  --source refund-window.lspx

vouch verify --reexecute --compiled-artifact refund-window.lpxvca и vouch gate --compiled-artifact refund-window.lpxvca связывают точные внешние исходник и вход потребителя с политикой доверия, аутентификацией издателя и текущим согласием tree и Meaning. До запуска проверенной виртуальной машины Native заново выводит Core IR и байткод из исходника. Контейнер хранит эту линию, а inspect, validate, verify и gate предоставляют последовательные наблюдения для рабочего процесса Ваучера.

Куда дальше

Точный двоичный контракт и проверяющий модуль описаны в справочнике. Чтобы изучить разрешённый смысл до компиляции, вернитесь к руководству Core IR.

Байткод и виртуальная машина Rust · Сборка заранее скомпилированного продукта · Native CLI

Запуск проверенного байткода · Лиспекс