Контракт ограниченного вычислителя

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

Зафиксированный набор контрактов

Provider — точные Wasm-байты из manifest bundle, а не произвольная пересборка или строка версии Lispex. Пересборка наследует гарантии только при идентичном SHA-256.

ABI и жизненный цикл

У модуля ноль imports, одна memory с 18 начальными и 256 максимальными страницами и только функции allocation, deallocation, ABI version, prepare и evaluate вместе со стандартными globals границ memory. Запросы ограничены, length-delimited и используют big-endian.

Каждая операция получает новые Wasmtime Store, Instance, memory, allocator, guest heap, interner, cells, continuations, meter, transcript и result buffer. Неизменяемый compiled Module можно разделять только по точному SHA-256 Wasm. 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 или шириной указателя. Charge происходит до эффекта, не возвращается, использует полный u64 и сообщает первую ось, чья следующая reservation превысила лимит. Proper tail calls не расходуют non-tail semantic frames.

Использованный и оставшийся бюджет не входит в portable core. Изменение тарифа, оси, единицы, порядка, overflow, depth или правила отказа требует нового model ID; бюджеты между моделями не переводятся.

Identity и core

Core разделяет identities точных представленных байтов, canonical source, семантического правила, canonical input, resource contract, запроса, артефакта вычислителя, вычисления, transcript и результата. Hash framing следует length-delimited SHA-256 контракту lispex.evaluation-identity/v1.

Core получают только детерминированный семантический исход и детерминированный отказ запроса. Операционное прерывание и engine fault не могут иметь core. Издатель может подписать готовые байты core вне вычислителя, но envelope не меняет категорию.

Ограниченный профиль

Первый профиль допускает только закрытый набор операций, проверенный bundle. Обычный полный tree-интерпретатор lispex-profile-1.5 остаётся отдельным. Неподдерживаемые формы и primitives отклоняются до VM. Provider не вызывает tree, продукты маршрутов Rust, Topaz, AOT, старый вычислитель или fallback.

Контракт Native-каталога решения

Native-обёртка rule представляет ограниченный вычислитель как один атомарный локальный процесс:

rule run -> inspect -> verify -> replay

rule run принимает точные файлы исходника и строгого JSON, а также раздельные лимиты подготовки и вычисления. Объекты JSON становятся records, массивы — vectors; строки, булевы и точные целые сохраняют тип, а null становится пустым списком. Повторяющиеся ключи, inexact numbers, неподдерживаемые значения и лишние данные дают детерминированный отказ запроса.

Успешный запуск создаёт ровно пять обычных файлов:

Каталог создаётся без перезаписи существующего пути. inspect и verify ничего не выполняют. replay использует свежий экземпляр вычислителя и требует совпадения результата и portable core. Отсутствующие, изменённые, лишние файлы и символические ссылки отклоняются.

Этот процесс предоставляет Native-продукт. Он не восстанавливает и не хранит представленный исходник, не ищет другой вычислитель, не вызывает fallback, не обращается к host capability или удалённому сервису, не повышает Vouch evidence и не разрешает внешнее действие.

Распространение и хранение

Native содержит точные байты provider. Релиз также публикует Wasm bundle, manifest, golden vectors, материалы verifier, SBOM/dependency dispositions, safety evidence и append-only release-DAG records. Обновление безопасности создаёт новую artifact identity и admission. Старые receipts проверяются сохранёнными старыми байтами и контрактами, хотя такой artifact может быть запрещён для новых adversarial evaluations.

Evaluator component не имеет Topaz build dependency. Независимый AOT component сохраняет собственный точный pin компилятора Topaz. Consumer Topaz должен закрепить digest этого evaluator component в отдельном последующем релизе.

Что не гарантируется

Контракт не обеспечивает конфиденциальность, удостоверение издателя, полномочия Vouch, правильность правила, provenance, freshness, разрешение внешнего действия, сокрытие времени, изоляцию cache или устойчивость к microarchitectural side channels. Browser и второй embedded engine не входят в первый выпуск.

Дальше

Native workflow показан в Вычислении недоверенного правила.