Вычисление недоверенного правила

Эта страница описывает v1.13. Проверьте, является ли она текущим руководством: /version.json

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

Обычная команда lispex rule.lspx использует полнопрофильный tree-интерпретатор. Команда lispex embed нужна, когда правило должно выполняться в меньшем профиле lispex/r7rs-rule-embedded-core/1 с детерминированными лимитами работы и логического выделения.

Native-файл содержит один точный Wasm-вычислитель без imports. Нельзя передать путь к другому вычислителю, обнаружить или скачать замену либо запросить fallback.

На странице загрузок также доступны точный lispex-embed-evaluator.wasm, manifest компонента, golden vectors и файлы SHA-256 для приложений, которые напрямую потребляют байты provider.

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

Создайте prepare-limits.json:

JSON

{
  "raw_source_bytes": 4096,
  "prepare_work": 1000000,
  "logical_allocation": 1000000,
  "syntax_depth": 64
}

Подготовьте исходный текст:

lispex embed prepare \
  --source policy.lspx \
  --limits prepare-limits.json \
  --out policy.lpxembed

Подготовка принимает UTF-8, читает и нормализует программу, создаёт и проверяет canonical bytecode и проверяет ограниченный профиль. Она записывает identities представленного и canonical исходника, семантического правила, набора возможностей, bytecode, вычислителя и точных лимитов, но не выполняет правило.

2. Выполните подготовленное правило

Вход — одно canonical-значение lispex.embed-value/v1. Создайте evaluation-limits.json:

JSON

{
  "canonical_input_bytes": 4096,
  "eval_work": 1000000,
  "logical_allocation": 1000000,
  "semantic_frames": 1000,
  "traversal_depth": 256,
  "output_bytes": 1000000,
  "diagnostic_bytes": 1000000,
  "transcript_bytes": 1000000,
  "transcript_events": 100,
  "result_bytes": 1000000
}

Выполните именно этот подготовленный артефакт:

lispex embed evaluate \
  --prepared policy.lpxembed \
  --input input.lpxvalue \
  --limits evaluation-limits.json \
  --out result.lpxembed

Расход подготовки никогда не входит в расход вычисления. Поэтому повторное использование подготовленного артефакта не меняет тариф вычисления или portable core.

3. Просмотрите и проверьте

lispex embed inspect --artifact result.lpxembed
lispex embed verify --artifact result.lpxembed

inspect показывает стабильную JSON-проекцию. verify без запуска правила пересчитывает envelope, точные хэши, категорию, лимиты и portable core. Эти команды не удостоверяют издателя и не создают полномочий Vouch.

Сначала прочитайте категорию

Категория	Значение	Portable core
детерминированный семантический исход	детерминированно получены значения, runtime-диагностика, исчерпание ресурса или непереносимый результат	да
детерминированный отказ запроса	точный запрос отклонён до допущенного вычисления	да
операционное прерывание	вызывающая сторона отменила работу или исполнитель остановился до результата	нет
сбой движка	вычислитель, ABI, allocator или safety ceiling нарушил контракт	нет

Израсходованная работа полезна как локальная диагностика, но не входит в portable core. Core связывает точные лимиты, профиль, модель, исходник, вход, запрос, артефакт вычислителя, transcript и результат.

Границы

Первый продукт использует один движок, а не согласование во время вызова. Точные байты проверяются дифференциальными судами уровня релиза. Ограниченный профиль меньше полного lispex-profile-1.5; неподдерживаемые формы и primitives отклоняются, а не передаются другому маршруту.

Поверхность предоставляют Native и отдельный bundle вычислителя. npm, публичный browser-WASM facade, Playground и browser embedding её не предоставляют. Timing-, cache- и microarchitectural side channels находятся вне технической гарантии. Выживание host process в первом in-process выпуске является операционной целью, а не гарантией безопасности.

Артефакт и core — материал для проверки, а не подпись Vouch, удостоверенное evidence, gate grant, доказательство правильности правила или разрешение на внешнее действие.

Дальше

Точные ID, оси, категории и контракт bundle описаны в контракте ограниченного вычислителя.