Bounded Evaluator Contract

This page describes v1.13. Verify whether it is the current manual at /version.json

Frozen contract set

The provider is the exact Wasm bytes named by the bundle manifest, not an arbitrary rebuild or a Lispex version label. A rebuild inherits the guarantee only when its SHA-256 is identical.

ABI and lifecycle

The module has zero imports, one memory with 18 initial and 256 maximum pages, and only the allocation, deallocation, ABI-version, prepare, and evaluate functions plus standard memory boundary globals. Requests are bounded, length-delimited, big-endian values.

Every operation gets a fresh Wasmtime Store, Instance, memory, allocator, guest heap, interner, cells, continuations, meter, transcript, and result buffer. An immutable compiled Module may be shared only under the exact Wasm SHA-256. Instance pooling is not admitted.

Separate resource domains

Preparation owns raw_source_bytes, prepare_work, prepare_logical_allocation, and syntax_depth. Evaluation owns canonical_input_bytes, eval_work, eval_logical_allocation, semantic_frames, traversal_depth, output_bytes, diagnostic_bytes, transcript_bytes, transcript_events, and result_bytes.

Work is a versioned deterministic tariff, not CPU time. Logical allocation is defined by the model, not Rust object size, allocator capacity, or pointer width. Charges occur before effects, never refund, use full u64, and fail on the first reservation that would exceed its named limit. Proper tail calls do not consume semantic non-tail frames.

Consumed or remaining usage is never part of the portable core. A tariff, axis, unit, ordering, overflow, depth, or failure-rule change creates a new model ID; budgets are not converted between models.

Identity and core

The core separates exact submitted-source bytes, canonical source, semantic rule, canonical input, resource contract, request, evaluator artifact, evaluation, transcript, and result identities. Hash framing is the normative lispex.evaluation-identity/v1 length-delimited SHA-256 construction.

Only deterministic semantic outcomes and deterministic request refusals carry a core. Operational interruptions and engine faults cannot carry one. An issuer may sign completed core bytes outside the evaluator, but that envelope does not change their category.

Restricted profile

The first profile admits the closed operation set qualified by the bundle. The ordinary full lispex-profile-1.5 tree interpreter remains separate. Unsupported forms or primitives fail closed before VM execution. The provider does not invoke tree, Rust route products, Topaz, AOT, an older evaluator, or any fallback.

Distribution and retention

Native contains the exact provider bytes. The release also publishes the Wasm bundle, manifest, golden vectors, verifier material, SBOM/dependency dispositions, safety evidence, and append-only release-DAG records. A security update creates a new artifact identity and admission; old receipts remain verifiable with retained old bytes and contracts but may be refused for new adversarial evaluation.

The evaluator component has no Topaz build dependency. The independent AOT component keeps its own exact Topaz compiler pin. A Topaz consumer must pin this evaluator component by digest in a later, separately admitted release.

Non-guarantees

The contract does not provide confidentiality, issuer authentication, Vouch authority, rule correctness, provenance, freshness, external-action authorization, timing secrecy, cache isolation, or microarchitectural side-channel resistance. Browser support and a second embedded engine are not part of the first release.

Keep going

Use Evaluate an Untrusted Rule for the Native workflow.