Замороженный набор контрактов
| Контракт | Идентификатор |
|---|---|
| семантический профиль | lispex/r7rs-rule-embedded-core/1 |
| модель работы и логического выделения | lispex-vm-meter/1 |
| codec значений | lispex.embed-value/v1 |
| transcript | lispex.embed-transcript/v1 |
| интерфейс WebAssembly | lispex.embed-wasm-abi/v1 |
| переносимое ядро | lispex.embed-receipt-core/v1 |
Переносимое ядро представляет собой ту часть записи, которая может передаваться сама по себе. Что именно оно связывает, перечислено ниже в разделе про identity и core.
Provider состоит из точных байтов WebAssembly, названных в манифесте пакета, а не из произвольной пересборки или строки версии Лиспекса. Пересборка наследует гарантии только при идентичном SHA-256.
Отдельный component полного текущего профиля
Публичный full component не является переименованным restricted profile. Он
добавляет отдельный семантический профиль
lispex/r7rs-rule-current-profile-bounded/1, модель подсчёта работы
lispex-full-vm-meter/1 и identity компонента
lispex-evaluator/rust-vm-current-profile/1 для всех 205 генерируемых строк
primitives при нуле Deferred. Существующие интерфейс, value codec, transcript и
schema переносимого ядра признаны достаточными и сохраняют точный смысл v1.
Full artifacts используют отдельный конверт LPXFAR01, а restricted
LPXART01 и исторические квитанции не меняются.
Интерфейс и жизненный цикл
Интерфейсом здесь называется закреплённый набор функций модуля и закреплённый способ передавать данные внутрь и наружу. У модуля ноль imports, одна memory с 18 начальными и 256 максимальными страницами и только функции allocation, deallocation, версии интерфейса, prepare и evaluate вместе со стандартными globals границ memory. Запросы ограничены по размеру, length-delimited и используют big-endian.
Каждая операция получает новые Wasmtime Store, Instance, memory, allocator, guest heap, interner, cells, продолжения, счётчик работы, transcript и result buffer. Неизменяемый compiled Module можно разделять только по точному SHA-256 WebAssembly. Instance pooling не допускается.
Раздельные области ресурсов
Подготовка владеет raw_source_bytes, prepare_work,
prepare_logical_allocation и syntax_depth. Вычисление владеет
canonical_input_bytes, eval_work, eval_logical_allocation,
semantic_frames, traversal_depth, output_bytes, diagnostic_bytes,
transcript_bytes, transcript_events и result_bytes.
Work представляет собой версионированный детерминированный тариф, а не CPU
time. Logical allocation задаётся моделью, а не размером объекта Rust,
capacity allocator или шириной указателя. Списание происходит до эффекта, не
возвращается, использует полный u64 и сообщает первую ось, чья следующая
reservation превысила бы лимит. Правильные хвостовые вызовы не расходуют
non-tail semantic frames.
Использованный и оставшийся бюджеты не входят в переносимое ядро. Изменение тарифа, оси, единицы, порядка, overflow, depth или правила отказа требует нового model ID, и бюджеты между моделями не переводятся.
Identity и core
Core разделяет identities точных представленных байтов, исходника в его
единственной закреплённой форме, семантического правила, ввода в его
единственной закреплённой форме, resource contract, запроса, артефакта,
который выполнил правило, вычисления, transcript и результата. Hash framing
следует length-delimited SHA-256 контракту lispex.evaluation-identity/v1.
Core получают только детерминированный семантический исход и детерминированный отказ запроса. Операционное прерывание и engine fault не могут иметь core. Издатель может подписать готовые байты core вне программы, которая выполняет правило, но конверт не меняет категорию.
Ограниченный профиль
Первый профиль допускает только закрытый набор операций, проверенный пакетом.
Обычный полный tree-интерпретатор lispex-profile-1.5 остаётся отдельным.
Неподдерживаемые формы и primitives отклоняются до того, как виртуальная
машина что-либо выполнит. Provider не вызывает tree, продукты маршрутов Rust,
Топаза, продукт, скомпилированный заранее, прежнюю программу для выполнения
правил или запасной путь.
Контракт Native-каталога решения
Native-обёртка rule представляет этот ограниченный исполнитель как один
атомарный локальный процесс.
rule run -> inspect -> verify -> replayrule run принимает точные файлы исходника и строгого JSON, а также
раздельные лимиты подготовки и вычисления. Объекты JSON становятся записями,
массивы становятся векторами, строки, булевы и точные целые сохраняют тип, а
null становится пустым списком. Повторяющиеся ключи, неточные числа,
неподдерживаемые значения и лишние данные дают детерминированный отказ
запроса.
Успешный запуск создаёт ровно пять обычных файлов.
| Файл | Роль |
|---|---|
prepared.lpxembed | точный подготовленный артефакт правила |
canonical-input.lpxvalue | ввод в его единственной закреплённой форме |
result.lpxembed | детерминированный исход и точная связь запроса |
receipt-core.lpxreceipt | допустимое переносимое ядро |
summary.json | производная неавторитетная сводка |
Каталог создаётся без перезаписи существующего пути. inspect и verify
ничего не выполняют. replay использует свежий экземпляр исполнителя и
требует совпадения результата и переносимого ядра. Отсутствующие, изменённые,
лишние файлы и символические ссылки отклоняются.
Этот процесс предоставляет Native-продукт. Он не восстанавливает и не хранит представленный исходник, не ищет другую программу для выполнения правила, не вызывает запасной путь, не обращается к host capability или удалённому сервису, не превращает запись в свидетельство Ваучера и не разрешает внешнее действие.
Распространение и хранение
Native содержит точные байты provider. Релиз также публикует пакет WebAssembly, манифест, эталонные векторы, материалы verifier, перечень программных компонентов и dependency dispositions, safety evidence и append-only release-DAG records. Обновление безопасности создаёт новую artifact identity и admission. Старые квитанции проверяются сохранёнными старыми байтами и контрактами, хотя для новых adversarial evaluations такие старые квитанции могут быть отклонены.
Этот component не имеет зависимости сборки от Топаза. Отдельный component, скомпилированный заранее, сохраняет собственный точный pin компилятора Топаза. Топаз как потребитель должен закрепить этот component по его точному хешу в отдельном последующем релизе.
Что не гарантируется
Контракт не обеспечивает конфиденциальность, удостоверение издателя, полномочия Ваучера, правильность правила, provenance, freshness, разрешение внешнего действия, сокрытие времени, изоляцию cache или устойчивость к microarchitectural side channels. Поддержка браузера не входит в этот выпуск.
Куда дальше
Native workflow показан в Вычислении недоверенного правила.